Home‎ > ‎

Verifying Java Card Programs with KeY

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:

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


ċ
KeY-1.6.0.zip
(7284k)
Wojciech Mostowski,
Jun 16, 2011, 5:51 AM
ċ
KeYExtLib-1.6.zip
(1502k)
Wojciech Mostowski,
Jun 16, 2011, 5:51 AM
ċ
examples.zip
(1k)
Wojciech Mostowski,
Jun 16, 2011, 5:55 AM
ċ
javacard_key.zip
(184k)
Wojciech Mostowski,
Jun 16, 2011, 5:54 AM
Ċ
slides.pdf
(546k)
Wojciech Mostowski,
Jun 19, 2011, 3:14 AM
Comments