Bibliography

1

G. Barthe, D. Gurov, and M. Huisman.
Compositional verification of secure applet interactions.
In Proc. FASE'02, volume 2306 of Lecture Notes in Computer Science, pages 15-32. Springer, 2002.

2

P. Bieber, J. Cazin, P. Girard, J.-L. Lanet, V. Wiels, and G. Zanon.
Checking secure interactions of smart card applets.
In ESORICS, pages 1-16, 2000.

3

A. Bouajjani, J. Esparza, and O. Maler.
Reachability analysis of pushdown automata: Application to model-checking.
In Proc. CONCUR'97, volume 1243 of Lecture Notes in Computer Science, pages 135-150. Springer, 1997.

4

O. Burkart, D. Caucal, F. Moller, and B. Steffen.
Verification on infinite structures.
In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 545-623. North Holland, 2000.

5

N. Cataño and M. Huisman.
Formal specification of Gemplus' electronic purse case study.
In Proc. FME'02, Lecture Notes in Computer Science. Springer, 2002.
To appear.

6

J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, and H. Zheng.
Bandera: extracting finite-state models from Java source code.
In International Conference on Software Engineering, pages 439-448, 2000.

7

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon.
Efficient algorithms for model checking pushdown systems.
In Proc. CAV'00, volume 1855 of Lecture Notes in Computer Science, pages 232-247. Springer, 2000.

8

J. Esparza and S. Schwoon.
A BDD-based model checker for recursive programs.
In Proc. CAV'01, volume 2102 of Lecture Notes in Computer Science, pages 324-336. Springer, 2001.

9

A. Finkel, B. Willems, and P. Wolper.
A direct symbolic approach to model checking pushdown systems.
In Electronic Notes in Theoretical Computer Science, volume 9, 1997.

10

K. Havelund and T. Pressburger.
Model checking Java programs using Java pathfinder.
International Journal on Software Tools for Technology Transfer, 2(4):366-381, 2000.

11

R. Iosif, C. Demartini, and R. Sisto.
Modeling and validation of Java multithreading applications using spin, 1998.

12

JavaCard 2.1.1 Documentation.
Technical report, Sun Microsystems, May 2000.
http://java.sun.com/products/javacard/specs.html#211.

13

T. Jensen, D. Le Metayer, and T. Thorn.
Verification of control flow based security properties.
In IEEE Symposium on Security and Privacy, pages 89-103, 1999.

14

R. Leino, G. Nelson, and J. Saxe.
ESC/Java User's Manual.
Technical Report 2000-004, Compaq Systems Research Center, October 2002.