Interactive verification of concurrent systems using symbolic execution

S. Bäumler, M. Balser, F. Nafz, W. Reif and G. Schellhorn

A proof method is described which combines compositional proofs of inter- leaved parallel programs with the intuitive and highly automatic strategy of symbolic execution. As logic we use an extended variant of Interval Temporal Logic that al- lows 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 01.03.2010 European Journal on Artificial Intelligence (AI Communications), Vol. 23, Number 2-3 / 2010, p. 285-307, DOI 10.3233/AIC-2010-0458

Publisher: IOS Press

ISBN: 0921-7126