A Dynamic Logic for Deductive Verification of Concurrent Programs
Bernhard Beckert and Vladimir Klebanov
In this paper, we present an approach aiming at full functional 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.