Verifying Concurrent Systems with Symbolic Execution
- 1 August 2002
- journal article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 12 (4) , 549-560
- https://doi.org/10.1093/logcom/12.4.549
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 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
This publication has 0 references indexed in Scilit: