document: Verifying concurrent systems with symbolic execution 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
doc_bio_tags: O B I O B I O O O O O B I O B I O B I O B I O O B I I O O O O O O O O O O O O O O O B I B I O O O O O O O O O O O O O O O O O B I O O O O O O O O O O O O O B I I I O O O O O O O O O O O O O O O B I