The KeY Approach: Integrating Design and Formal Verification
of Java Card Programs
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese,
Elmar Habermalz, Reiner Haehnle, Wolfram Menzel, and Peter H. Schmitt
This paper reports on the ongoing KeY project aimed at bridging the gap
between (a) object-oriented software engineering methods and tools and
(b) deductive verification for the development of Java Card programs. In
particular, we describe a Dynamic Logic for Java Card and outline a
sequent calculus for this logic that axiomatises Java Card and is used
in the verification component of the KeY system.