Formal Specification and Verification of JavaCard's Application Identifier Class

Abstract This note discusses a verification in PVS of the AID (Application Identifier) class from JavaCard's API. The properties that are verified are formulated in the interface specification language JML. This language is also used to express the properties that are assumed about the native methods from the Util class that are used in the AID class.

• Type: Conference
• Year: 2000
• Where: JAVACARD
• Authors: Joachim van den Berg, Bart Jacobs, Erik Poll
• Keywords: JAVACARD 2000, JavaCard's API, Programming Languages, Specification Language Jml, Util Class