The latest generation of smart cards i developed for multiple applications. There is a small operating system on-card together with a virtual machine, an API and some cryptographic machinery.

These cards are capable of executing small JavaCard programs, called applets, for instance for banking or communication (GSM). JavaCard is a stripped-down version of Java, designed to run in an environment with limited resources.

Since these cards are especially used for security sensitive application, correctness is an important issue. In this talk it will be argued that such smart cards form an ideal target (and challenge) for formal methods, because:
- the programs that run on these cards are very small, and within the reach of modern verification tools;
- these cards are distributed in large numbers, so that flaws can have a huge impact;
- the smart card industry is driven by certification demands in which formal medthods are important

This talk will focus on the work done at Nijmegen on applet specification, with the spcification language JML, for Java Modeling Language (see http://www.cs.iastate,edu/~leavens/JML.html), and verification with the prooftool PVS (see http://www.pvs.csl.sri.com ). It will show several sample verifications and explain the program logics that are used.