A Dynamic Logic for Deductive Verification of Concurrent Programs
Bernhard Beckert, Vladimir Klebanov · 2007
In this paper, we present an approach aiming at full junctional deductive verification of concurrent Java programs, based on symbolic execution. We define a dynamic logic and a deductive verification calculus for a restricted fragment of Java with native concurrency primitives. Even though we cannot yet deal with non-atomic loops, employing the technique of symmetry reduction allows us to verify unbounded systems. The calculus has been implemented within the KeY system, and we demonstrate it by verifying a central method of the StringBuffer class from the Java standard library.