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

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Simon Bäumler, Florian Nafz, Michael Balser, Wolfgang Reif
• Keywords: Automated Reasoning, CADE 2008, Interactive Proof Method, Interval Temporal Logic, Proof Method