Verification of JavaCard programs

This report is concerned with the formal verification of JavaCard programs, or sequentiel Java programs. A calculus in dynamic logic is presented. This calculus is implemented in KIV, and ready for use. It is the first implemented proof system for JavaCard. KIV parses the original JavaCard (or Java) program, resolves names and types in the same manner as a normal Java compiler, and produces an annotated abstract syntax tree that is the input for the verification. All sequential Java statements (i.e. all Java statements except synchronized), and all Java expressions are handled. Exceptions, breaks, static initialization, objects, dynamic method lookup, and arrays are supported. This report is intended as a reference manual for the calculus. The abstract syntax of Java programs, the proof rules, and the underlying algebraic specifications for the object store and the primitive data types, and a formal semantic is described in detail. An example proof and a list of validation programs conclude the report