title: Verifying concurrent systems with symbolic execution
abstract: 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 adopt this technique for parallel programs. Properties are formulated in interval temporal logic. An implementation in the interactive theorem prover KIV has shown that this technique offers a high degree of automation and allows simple, local invariants
keyphrases: concurrent systems symbolic execution temporal properties transition systems temporal formulas program counter variables sequential programs parallel programs interactive theorem prover KIV local invariants concurrent systems verification