Compositional Proofs with Symbolic Execution

Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif

Compositional Proofs with Symbolic Execution

A proof method is described which combines compositional proofs of interleaved parallel programs with the intuitive and highly automatic strategy of symbolic execution. As logic we use an extended variant of Interval Temporal Logic that allows to formulate programs directly in the Simple Programming Language (SPL). The notation includes a complex interleaving operator. The interactive proof method we use for temporal properties is symbolic execution with induction. Here, we show how to combine this proof method with an assumption-guarantee approach to decompose proofs for safety properties. We demonstrate the application of this technique with a producer-channel-consumer case study.
published 2008 Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008 Sydney, Australia, August 10-11, 2008.

Publisher: CEUR Workshop Proceedings, Vol. 372