Proceedings, Java Card Workshop
Bernhard Beckert
A Dynamic Logic for the Formal Verification of Java Card Programs
In this paper, we define a program logic (an instance of Dynamic Logic)
for formalising properties of Java Card programs, and we give a sequent
calculus for formally verifying such properties. The purpose of this
work is to provide a framework for software verification that can be
integrated into real-world software development processes.