Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 4, August 2002: pp. 549-560

Verifying Concurrent Systems with Symbolic Execution

Michael Balser1, Christoph Duelli1, Wolfgang Reif1 and Gerhard Schellhorn1

1Lehrstuhl Softwaretechnik und Programmiersprachen, Universität Augsburg, D-86135 Augsburg, Germany. Email: {balser,duelli,reif,schellhorn}@informatik.uni-augsburg.de

Current techniques for interactively proving temporal properties of concurrent systems translate transition systems into temporal formulas by introducing program counter variables. Proofs are not intuitive, because control flow is not explicitly considered. For sequential programs symbolic execution is a very intuitive, interactive proof strategy. In this paper we will adopt this technique for parallel programs. Properties are formulated in interval temporal logic. An inplementation in the interactive theorem prover KIV has shown that this technique offers a high degree of automation and allows simple, local invariants.

Keywords: Symbolic execution; induction; temporal logic; parallel program; concurrent system; program verification

Table of Contents   Full-Text PDF (142 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement