Technische Universität München, Department of Computer Science, Software & Systems Engineering up: Isabelle Group

VerifiCard @ Munich


Project Description

The project VerifiCard is concerned with the formalization of aspects of JavaCard, a subset of the Java language deployed on smartcards.

VerifiCard @ Munich is part of the EU-sponsored project VerifiCard which involves partners from academia and industry. The focus of our group is on formalization and machine-aided analysis of

Formalization and verification are carried out in the theorem proving environment Isabelle/HOL.

Project Members


(see list of all Verificard deliverables)



Isabelle Formalizations

There are two Isabelle formalizations of Java: Both formalizations are also included in the current Isabelle distribution.

JavaCard source language

(VerifiCard deliverable for Tasks 2.1 and 2.2)

JavaCard bytecode language

(VerifiCard deliverable for Tasks 3.1 and 3.3)

The Java bytecode verifier with object initialization: A formalization of the Java bytecode verifier, including a defensive JVM, exceptions, constructor calls, object initialization, jsr/ret instructions, and arrays:


(VerifiCard deliverable for Task 3.4)


Some teaching activities related to the topics of VerifiCard (in German):
Martin Strecker
URL:, Last modified: Mon Nov 24 15:05:11 MET 2003