Apr 24, 2012: Wojciech Mostowski: Verification of Java Card Programs with Transactions using Explicit Heaps

April 24, 2012Verification of Java Card Programs with Transactions using Explicit Heaps
Room: Zi 5126Wojciech Mostowski

In the context of the KeY program verifier we discuss a redesign of the KeY Dynamic Logic calculus to handle the intricacies of the Java Card transaction mechanism, a smart card specific addition to Java program semantics. The KeY system was the first verification tool to faithfully formalise Java Card transactions.  However, in light of recent developments to base the KeY calculus on the idea of dynamic frames and explicit heap representation, the existing Java Card support, being "incompatible", had to be dropped.  We present the reconstruction of this support on top of the new explicit heap representation. The new, fully implemented solution is considerably simpler than the old one in turn enabling smaller than before proofs for Java Card programs. This further justifies the use of explicit heaps in program calculi. In the course of this work, also the specification language JML* was extended.  The commencing work to support concurrency in KeY by adding permissions to the logic also entails extensions to JML*. Common features observed in both designs show a possible need to treat heap structures as first class citizens also in specification languages.