CertiCartes is a formalisation in Coq of the JavaCard platform. It contains formal executable specifications of the defensive JavaCard Virtual Machine and the abstract virtual machine.
Coq version 7.0 is needed to use this formalisation.
Download Certicartes (tar.gz format) - a makefile is included in the archive.
Browse the files from the archive.