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.