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.

• Type: Conference
• Year: 2004
• Where: AMAST
• Authors: Kurt Stenzel
• Keywords: AMAST 2004, Java Language Constructs, Sequential Java Programs, Smart Card Applications, Software Engineering