|
|
Nieuws III
[CSI]TODAY: Engelbert Hubbers, 26 April 2004
Today, Mon Apr 26 2004 at 16:00:00 sharp,
dr. Engelbert Hubbers
of the SOS group of the NIII will give a talk in CZN8. There will becoffee and health-food cookies in the hall 15 minutes before the talkstarts.
"Reasoning about transactions in Java Card"
With the LOOP/PVS combination we have infrastructure to reason about JMLannotated Java code. Since Java Card is usually considered to be a subsetof Java, this setup should also work for reasoning about Java Cardapplets. However, if we look more precise, we see that it is not a strictsubset: Java Card has transient memory and a transaction mechanism notavailable in Java. In this talk I present a method that allows to reasonabout this kind of peculiarities.
This is joint work with Erik Poll.
Huidig
|
|
|
