SucheA Formally Verified Calculus for Full Java Card
K. Stenzel
A Formally Verified Calculus for Full Java Card
We present a calculus for the verification of sequential Java
programs. It supports all Java language constructs and has additional
support for Java Card. The calculus is formally proved correct with respect
to a natural semantics. It is implemented in the KIV system and
used for smart card applications.
C. Rattray, S. Maharaj, and C. Shankland (editors), Algebraic Methodology and Software Technology (AMAST) 2004 Proceedings. Stirling Scotland, July 2004. Springer LNCS 3116
Downloads:
- download pdf version - (javacard-calculus-amast2004-pdf.pdf, 239 KB)
- download postscript version - (javacard-calculus-amast2004-ps.ps, 221 KB)