A Java Card CAP converter in PVS1 1This work was partially funded by the European IST R&D project 2000-26328 “Verifi card”
Thomas Genet, Thomas Wiben Jensen, Vikash Kodati, David Pichardie · Electronic Notes in Theoretical Computer Science · 2004
The Java Card language is a trimmed down dialect of Java aimed at programming smart cards. Java Card specifies its own class file format (the Java Card Converted APplet (CAP) format) that is optimised with respect to the limited space resources of smart cards. This paper deals with the certified development of algorithms necessary for the conversion of ordinary Java class files into the CAP format. More precisely, these algorithms are concerned with constructing and compressing method tables and constant pools. The main contribution of this paper is to specify and prove the correctness of these algorithms using the theorem prover PVS.