ISSE

Search

A 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: