A Dynamic Logic for Java Card

Bernhard Beckert


In this paper, I describe a Dynamic Logic for Java Card and outline a
sequent calculus for this logic that axiomatises Java Card.  The purpose
of the logic is to provide a framework for software verification that
can be integrated into real-word software development processes.