Verifying concurrent systems with symbolic execution [Elektronische Ressource] : temporal reasoning is symbolic execution with a little induction / von Michael Balser

Verifying Concurrent SystemswithSymbolic ExecutionTemporal Reasoning is Symbolic Execution with a Little InductionDissertationzur Erlangung des Doktorgrades Dr. rer. nat.der Fakult¨at fu¨r Angewandte Informatikder Universit¨at Augsburgim Jahr 2005 vonMichael BalserONSKABUCGRHO0MiiAmtierender Dekan: Prof. Dr. Wolfgang ReifGutachter: Prof. Dr. Wolfgang ReifProf. Dr. Walter VoglerTag der Pruf¨ ung: 12. Juli 2005Pruf¨ er: Prof. Dr. Wolfgang ReifProf. Dr. Bernhard BauerProf. Dr. Bernhard Mo¨lleriiiAbstractSymbolic execution is an intuitive strategy to verify sequential programs, which can beautomated to a large extent. We have successfully carried over this method of proof tothe interactive verification of concurrent systems. The resulting strategy can be appliedto the verification of complex parallel programs and arbitrary (linear) temporal formulas.Our underlying logic is defined such that operators for parallel programs and temporallogic can be arbitrarily nested. We support interleaving with explicit blocking, nonde-terministic choice, and others. Most important, the semantics of all of the operators arecompositional. Thus, systems can be abstracted and proofs can be decomposed. Thisensures that our strategy of proof can be applied to the verification of large, concurrentsystems.