Tutorial at CADE-20

Integrating Object-oriented Design and
Deductive Verification of Software

Chapter

Deductive verification of implementations

This part of the tutorial focuses on how an implementation can be verified to be correct w.r.t. its specification using deductive techniques.

First, we present the basic version of Dynamic Logic (this program logic can be seen as an extension of Hoare logic). And then we describe an extended version of Dynamic Logic that allows to verify Java programs (we only consider the Java subset JavaCard, which in particular does not have concurrency).

Finally, we demonstrate how constraints on operations can be translated into Dynamic Logic proof obligations. And we show that, with tool support like in the KeY System (which uses a sequent calculus for dynamic logic), code examples involving non-trivial Java features (e.g., exception handling) can be verified.