Sciweavers

CADE
2008
Springer

Compositional Proofs with Symbolic Execution

14 years 3 months ago
Compositional Proofs with Symbolic Execution
Abstract. 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. 1
Simon Bäumler, Florian Nafz, Michael Balser,
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Simon Bäumler, Florian Nafz, Michael Balser, Wolfgang Reif
Comments (0)