Pink states for runtime verification

Quality and reliability of software programs are hugely important especially in safety-critical systems. Runtime verification ensures the correctness of an execution of a system by monitoring the system at runtime. It can be used in addition to incomplete verification techniques like testing and when complete techniques like model checking are not feasible. Runtime monitors should be predictive, i.e. report errors before they actually occur, as it allows an earlier reaction and the error might even still be avoided. In this thesis two predictive semantics for runtime verification are presented. They allow to take an abstraction of the underlying program into account to synthesize predictive monitors. As an example for such an abstraction the control-flow graph of a program is considered. Different procedures for synthesizing the corresponding monitors are developed and compared. One monitor procedure has been implemented in a prototype tool and evaluated on several example programs and correctness properties.