Open Access

Michael Balser

• Symbolic execution is an intuitive strategy to verify sequential programs, which can be automated to a large extent. We have successfully carried over this method of proof to the interactive verification of concurrent systems. The resulting strategy can be applied to the verification of complex parallel programs and arbitrary (linear) temporal formulas. Our underlying logic is defined such that operators for parallel programs and temporal logic can be arbitrarily nested. We support interleaving with explicit blocking, nondeterministic choice, and others. Most important, the semantics of all of the operators are compositional. Thus, systems can be abstracted and proofs can be decomposed. This ensures that our strategy of proof can be applied to the verification of large, concurrent systems.
• Symbolische Ausführung ist eine intuitive Technik zur Verifikation sequentieller Programme, welche einen hohen Automatisierungsgrad aufweist. In dieser Arbeit wird dieselbe Beweistechnik erfolgreich auf die interaktive Verifikation nebenläufiger Systeme übertragen. Mit der resultierenden Beweisstrategie können beliebige (lineare) temporallogische Eigenschaften für komplexe parallele Programme nachgewiesen werden. Die vorgestellte Logik erlaubt, Operatoren für parallele Programme und temporallogische Operatoren beliebig zu verschachteln, wobei komplexe Operatoren wie Interleaving von möglicherweise blockierten Prozessen und nichtdeterministische Auswahl unterstützt werden. Ein zentraler Aspekt dieser Arbeit ist, dass alle Operatoren kompositional sind. Systeme können abstrahiert und Beweise kompositional geführt werden. Dadurch ist die vorgestellte Beweisstrategie auch auf große, nebenläufige Systeme anwendbar.