Copenhagen Programming Language Seminar
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:
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.
Carsten Butz. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, IT-C and KVL.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org