2002 |
|
| [BartheC02] |
Efficient reasoning about executable specifications in Coq G. Barthe, P. Courtieu In C. Muñoz and S. Tahar, editors, the proceedings of TPHOLs'02 number 2410 of LNCS, pages 31 - 46, Springer-Verlag, 2002. © Springer-Verlag |
| [BartheCDS02] |
Tool-Assisted Specification and Verification of the JavaCard Platform G. Barthe, P. Courtieu, G. Dufay, S. Sousa In H. Kirchner and C. Ringeissen, editors, the proceedings of AMAST'02 number 2422 of LNCS, pages 41-59, Springer-Verlag, 2002. © Springer-Verlag |
[BartheDJSS02] |
A formal correspondence between offensive and defensive JavaCard
virtual machines. G. Barthe, G. Dufay, L. Jakubiec, S. Sousa In A. Cortesi, editor, the proceedings of VMCAI'02 number 2294 of LNCS, pages 32 - 45, Springer-Verlag, 2002. © Springer-Verlag |
| [BartheGH02] |
Compositional Verification of Secure Applet Interactions G. Barthe, D. Gurov, M. Huisman In R.-D. Kutsche and H. Weber, editors, the proceedings of FASE'02. Number 2306 of LNCS, pages 15-32. Springer-Verlag, 2002. © Springer-Verlag |
| [CatanoH02] |
Formal specification of Gemplus' electronic purse case study Néstor Cataño, M. Huisman In L-H. Eriksson and P.A. Lindsay, editors, the proceedings of FME 2002 number 2391 of LNCS, pages 272-289. Springer-Verlag, 2002. © Springer-Verlag |
| [Huisman02] |
Verification of Java's AbstractCollection class: a case study M. Huisman In E. Boiten and B. Möller, editors, the proceedings of MPC 2002 number 2386 of LNCS, pages 175-194. Springer-Verlag, 2002. © Springer-Verlag |
| [Perovich02] |
Secure Object Sharing Development Kit for JavaCard
D. Perovich |
| [TrentelmanH02] |
Extending JML with temporal logic
K. Trentelman, M. Huisman In H. Kirchner and C. Ringeissen, editors, the proceedings of AMAST'02 number 2422 of LNCS, pages 334-348, Springer-Verlag, 2002. © Springer-Verlag |
2001 |
|
| [BartheDHS01] |
Jakarta: a toolset for reasoning about JavaCard G. Barthe, G. Dufay, M. Huisman, S. Sousa In I. Attali and T. Jensen, editors, the proceedings of E-smart 2001 number 2140 of LNCS, pages 2 - 18. Springer-Verlag, 2001. © Springer-Verlag |
| [BartheDJSS01] |
A Formal Executable Semantics of the JavaCard Platform G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Sousa In D. Sands, editor, the proceedings of ESOP 2001 number 2028 of LNCS, pages 302 - 319. Springer-Verlag, 2001. © Springer-Verlag |
| [BartheGH01] |
Compositional specification and verification of
control flow based security properties of multi-application programs
G. Barthe, D. Gurov, M. Huisman, In S. Drossopoulou, editor, the proceedings of FTfJP 2001 2001 |
| [Bertot01] |
Formalizing a JVML verifier for initialization in a theorem prover Yves Bertot In G. Berry, H. Comon, A. Finkel, editors, the proceedings of CAV'01. number 2102 of LNCS, pages 14 - 24. Springer-Verlag, 2001. © Springer-Verlag |
| [Catano01] |
La clause modifiable de JML: Sémantique, Vérification et
Application
Néstor Cataño Rapport de Stage DEA Programmation: Sémantique, Preuves et Langages Université Paris VII - Denis Diderot 2001 |
2000 |
|
| [DenneyJ00] |
Correctness of Java Card method lookup via logical relations E. Denney, T. Jensen In G. Smolka, editor, the proceedings of ESOP 2000 number 1782 of LNCS, pages 104 - 118. Springer-Verlag, 2000. © Springer-Verlag |
1999 |
|
| [JensenMT99] |
Verification of control flow based security properties T. Jensen, D. Le Métayer, T. Thorn In the proceedings of 20th IEEE Security and Privacy Symposium, Oakland, CA 1999 An extended version is available as IRISA technical report, nº 1210 |