A Dynamic Logic for Deductive Verification of Concurrent Java Programs with
Condition Variables
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. In contrast to
previous work, the version presented here includes the rules for handling
condition variables.