The purpose of this tutorial is to get hands-on experience with verifying real Java Card programs. The KeY verification system is going to be used (download) with two case studies:

• Java Card API reference implementation,

• The open source implementation of the ISO18013 electronic driving license, see http://sourceforge.net/projects/isodl/

Corresponding introductory material will be provided during a short presentation followed by practical work with KeY. The exact scope of this practical work will be dynamically allocated depending on the number of participants and their experience. The participants should have access to a laptop with a working JDK installation. Pre-installed KeY system is not necessary, but will certainly save time during the session. Before the tutorial I also recommend quick browsing of the links provided in this summary as well as reading the following:

Wojciech Mostowski, Fully Verified Java Card API Reference Implementation. Proceedings of the Verify 2007 Workshop (PDF)

Tutorial Material

• Slides
• Slides examples
  
• KeY distribution
• https://sites.google.com/a/cost-ic0701.org/limerick/home/verifying-java-card-programs-with-key/KeY-1.6.0.zip
• https://sites.google.com/a/cost-ic0701.org/limerick/home/verifying-java-card-programs-with-key/KeYExtLib-1.6.zip
• KeY project for the session