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.