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.