|
9.00 - 10.30
|
Bart Jacobs, Univ. of Nijmegen: Overview of the Verificard project
(slides)
|
|
|
Chris Hankin, Imperial College: Overview of the Secsafe project
(slides)
|
|
10.30 - 11.00
|
Break
|
|
11.00 - 12.30
|
Nestor Cataño, Marieke Huisman, Inria:
A static checker for JML's assignable clause
(slides)
|
|
Cees-Bart Breunesse, Martijn Oostdijk, Erik Poll, Bart
Jacobs, Univ. Nijmegen: The Loop tool
(slides)
|
|
Arnd Poetzsch-Heffter, Univ. Kaiserslautern: Jive: a verification tool
for Java Card
(slides)
|
|
12.30 - 14.00
|
Lunch
|
14.00 - 15.30
|
Renaud Marlet, Trusted Logic: Analyzing Java Card Programs: An
Industrial Perspective
(slides)
|
|
Rene Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, Tech. Univ. Denmark: Security Analysis for Carmel
(slides)
|
|
Boutheina Chetali, SchlumbergerSema: Formal methods at
SchlumbergerSema
|
|
15.30 - 16.00
|
Break
|
|
16.00 - 17.30
|
Erik Poll, Univ. Nijmegen: Java Card applet verification in JML
(slides)
|
|
Jean-Christophe Filliatre, Claude Marché, Christine Paulin
and Xavier Urbain, Inria: Modeling of Java programs in Coq
Slides available as:
See also the general Krakatoa page
|
|
Gennady Chugunov, Lars-Ake Fredlund and Dilian Gurov, Sics and KTH: Proving behavioural
properties of Java Card applets
(slides)
|
|
9.00 - 10.30
|
Igor Siveroni, Imperial College: An operational semantics of Java Card
(slides)
|
|
|
Frédéric Besson, Thomas de Grenier de Latour, Thomas Jensen, Inria: Secure calling contexts for stack inspection
(slides)
|
|
|
Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa, Inria: The Jakarta toolset
(slides)
|
|
10.30 - 11.00
|
Break
|
|
11.00 - 12.30
|
Pablo Giambiagi and Mads Dam, Sics : Confidentiality for
Protocol Implementations
(slides pdf)
(slides ps.gz)
|
|
|
Martin Strecker, Tech. Univ. Munchen: Compilation and bytecode
verification: Proving type correctness of generated bytecode in Isabelle
(slides)
|
|
|
Thomas Genet, Thomas Jensen, Vikash Kodati, Francois Monin, David Pichardie, Inria: A Java Card CAP converter in
PVS
(slides)
|