The dependability of the services provided by modern information systems heavily depends on the permanent design and implementation faults of the software and on the transient faults of the underlying hardware. Due to the ever-growing complexity of these systems, testing cannot detect and remove all possible software faults. These faults (similarly to hardware faults) may result in run-time failures. In the case of transient hardware faults, failures can be avoided by fault tolerance, i.e. reconfiguration and the recovery of the correct service. The prerequisite of fault tolerance is the early error detection. Both testing and fault tolerance require run-time verification, i.e. the concurrent monitoring and analysis of program execution. During testing, it provides information on the test coverage, while in run-time it supports on-line error detection and triggers the necessary recovery steps. The research aims at the elaboration of formally proven methods for the run-time verification of programs, which can be used during testing as well as during operation.