version française All team publications
Publications complete
[BibTeX Format]

[BK08a] G. Barthe and C. Kunz. Certificate translation for specification-preserving advices. In Proceedings of the Foundations of Aspect-Oriented Languages Workshop (FOAL), Brussels, Belgium, April 2008. ACM. [ bib | .pdf ]
[BK08b] G. Barthe and C. Kunz. Certificate translation in abstract interpretation. In Proceedings of the 17th European Symposium on Programming (ESOP), LNCS, Budapest, Hungary, March-April 2008. Springer-Verlag. [ bib | .pdf ]
[GHS08] D. Gurov, M. Huisman, and C. Sprenger. An algorithmic approach to compositional verification of sequential programs with procedures: An overview. In Foundations of Interface Technologies (FIT 2008), 2008. [ bib | .pdf ]
[HP08] Marieke Huisman and Gustavo Petri. BicolanoMT: a formalization of multi-threaded Java at bytecode level. In Bytecode 2008, Electronic Notes in Theoretical Computer Science, 2008. [ bib | .pdf ]
[HH07a] Marieke Huisman and Clément Hurlin. Permission specifications for common multithreaded programming patterns. In Reflections on Type Theory, Lambda Calculus, and the Mind. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday, 2007. [ bib | .pdf ]
[GH07] D. Gurov and M. Huisman. Reducing behavioural to structural properties of programs with procedures. Technical Report TRITA-CSC-TCS 2007:3, KTH Royal Institute of Technology, Stockholm, 2007. [ bib | .pdf | .pdf ]
[GS07] Benjamin Grégoire and Jorge Luis Sacchini. Combining a verification condition generator for a bytecode language with static analyses. 2007. To appear. [ bib ]
[BGJB07] Gilles Barthe, Bejamin Grégoire, Romain Janvier, and Santiago Zanella Béguelin. A framework for language-based cryptographic proofs. Oct 2007. [ bib ]
[HCF+07] Clément Hurlin, Amine Chaieb, Pascal Fontaine, Stephan Merz, and Tjark Weber. Practical proof reconstruction for first-order logic and set-theoretical constructions. In Lucas Dixon and Moa Johansson, editors, Isabelle Workshop (ISABELLE-WS), pages 2-13, Bremen, Germany, 2007. [ bib | .pdf ]
[HH07b] Marieke Huisman and Clément Hurlin. The stability problem for verification of concurrent object-oriented programs. In Verification and Analysis of Multi-threaded Java-like Programs (VAMP), 2007. To appear. [ bib | .pdf ]
[HP07] Marieke Huisman and Gustavo Petri. The Java memory model: a formal explanation. In Verification and Analysis of Multi-threaded Java-like Programs (VAMP), 2007. To appear. [ bib | .pdf ]
[HG07] Marieke Huisman and Dilian Gurov. Composing modal properties of programs with procedures. In Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007), 2007. [ bib | .pdf ]
[BHP07] Lilian Burdy, Marieke Huisman, and Mariela Pavlova. Preliminary design of BML: A behavioral interface specification language for Java bytecode. In Fundamental Approaches to Software Engineering (FASE 2007), volume 4422 of Lecture Notes in Computer Science, pages 215-229. Springer-Verlag, 2007. [ bib | .pdf ]
[BBC+07] G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova, and A. Requet. JACK: a tool for validation of security and behaviour of Java applications. In FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects, Lecture Notes in Computer Science. Springer-Verlag, 2007. To appear. [ bib | .pdf ]
[Pav07] M. Pavlova. Specification and verification of Java bytecode. PhD thesis, Université de Nice Sophia-Antipolis, 2007. [ bib ]
[BGP06] G. Barthe, B. Grégoire, and F. Pastawski. Type-based termination of recursive definitions in the calculus of inductive constructions. In Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06), Lecture Notes in Artificial Intelligence. Springer-Verlag, November 2006. To appear. [ bib | .pdf.gz | .ps.gz ]
[BGKR06] G. Barthe, B. Grégoire, C. Kunz, and T. Rezk. Certificate translation for optimizing compilers. In Proceedings of the 13th International Static Analysis Symposium (SAS), LNCS, Seoul, Korea, August 2006. Springer-Verlag. [ bib | .pdf ]
[HWS06] M. Huisman, P. Worah, and K. Sunesen. A temporal logic characterisation of observational determinism. In 19th IEEE Computer Security Foundations Workshop. IEEE Computer Society, July 2006. [ bib | .pdf ]
[Hur06] Clément Hurlin. Proof reconstruction for first-order logic and set-theoretical constructions. In Stefan Merz and Tobias Nipkow, editors, International Workshop on Automated Verification of Critical Systems (AVOCS), pages 157-162, 2006. [ bib | .pdf ]
[Tea06] Everest Team. Developer oriented methodology for applet validation, 2006. Inspired Deliverable 9.1. [ bib ]
[Cha06] J. Charles. Adding native specifications to JML. In Proceedings of the ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP'2006), 2006. [ bib | .ps ]
[ZBL06] Santiago Zanella Béguelin, Gustavo Betarte, and Carlos Luna. A formal specification of the MIDP 2.0 security model. In Theodosis Dimitrakos, Fabio Martinelli, Peter Y. A. Ryan, and Steve A. Schneider, editors, Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers, volume 4691 of Lecture Notes in Computer Science, pages 220-234. Springer-Verlag, 2006. [ bib | .pdf | http ]
[BP06] L. Burdy and M. Pavlova. Java bytecode specification and verification. In L.M. Liebrock, editor, proceedings of SAC'06. ACM, 2006. [ bib | .pdf ]
[BNR06b] G. Barthe, D. Naumann, and T. Rezk. Deriving an information flow checker and certifying compiler for Java. In Proceedings of Symposium of Security and Privacy'06. IEEE Press, 2006. [ bib | .ps ]
[BNR06a] G. Barthe, D. Naumann, and T. Rezk. Deriving an information flow checker and certifying compiler for Java, 2006. To appear. [ bib ]
[BPR06] G. Barthe, D. Pichardie, and T. Rezk. Deriving an information flow checker for the JVM. Technical report, INRIA, 2006. [ bib ]
[BFPR06] G. Barthe, J. Forest, D. Pichardie, and V. Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In M. Hagiya and P. Wadler, editors, Proceedings of FLOPS'06, volume 3945 of Lecture Notes in Computer Science, pages 114-129. Springer-Verlag, 2006. [ bib | .pdf | .ps.gz ]
[GTW06] B. Grégoire, L. Thery, and B. Werner. A computational approach to Pocklington certificates in type theory. In M. Hagiya and P. Wadler, editors, Proceedings of FLOPS'06, volume 3945 of Lecture Notes in Computer Science, pages 97 - 113. Springer-Verlag, 2006. [ bib | .pdf ]
[GT06] B. Grégoire and L. Thery. A purely functional library for modular arithmetic and its application for certifying large prime numbers. In U. Furbach and N. Shankar, editors, Proceedings of IJCAR'06, volume 4130 of Lecture Notes in Artificial Intelligence, pages 423-437. Springer-Verlag, 2006. [ bib | .pdf ]
[BDR06] G. Barthe, P. D'Argenio, and T. Rezk. Secure Information Flow by Self-Composition. Technical report, INRIA, 2006. [ bib ]
[Rez06] T. Rezk. Verification of confidentiality policies for mobile code. PhD thesis, Université de Nice Sophia-Antipolis, 2006. [ bib ]
[Tar06] S. Tarento. Formalisation en Coq de modeles cryptographiques et application au cryptosysteme ElGamal. PhD thesis, Université de Nice Sophia-Antipolis, 2006. [ bib ]
[CPGV06] A. Courbot, M. Pavlova, G. Grimaud, and J.J. Vandewalle. A low-footprint Java-to-native compilation scheme using formal methods. In J. Domingo-Ferrer, J. Posegga, and D. Schreckling, editors, proceedings of CARDIS, volume 3928 of Lecture Notes in Computer Science, pages 329-344. Springer, 2006. [ bib ]
[GHS06] D. Gurov, M. Huisman, and C. Sprenger. Compositional verification of sequential programs with procedures. Technical report, INRIA, 2006. [ bib ]
[BBC+06] Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, and Eric Vétillard. Mobius: Mobility, ubiquity, security. objectives and progress report. In TGC 2006: Proceedings of the second symposium on Trustworthy Global Computing, LNCS. Springer-Verlag, 2006. [ bib | .pdf ]
[BPS05] G. Barthe, M. Pavlova, and G. Schneider. Precise analysis of memory consumption using program logics. In B. Aichernig and B. Beckert, editors, Proceedings of SEFM'05, pages 86-95, Koblenz, Germany, September 2005. IEEE Computer Society. [ bib | .pdf ]
[GH05] D. Gurov and M. Huisman. Interface abstraction for compositional verification. In B. Aichernig and B. Beckert, editors, Proceedings of SEFM'05, pages 414-423, Koblenz, Germany, September 2005. IEEE Computer Society. An earlier version appeared as INRIA Technical Report, nr. RR-5330. [ bib | .ps.gz ]
[GM05] B. Grégoire and A. Mahboubi. Proving equalities in a commutative ring done right in Coq. In J. Hurd and T. Melham, editors, Proceedings of TPHOLs'05, volume 3603 of Lecture Notes in Computer Science, pages 98-113, Oxford, UK, August 2005. Springer-Verlag. [ bib | .ps.gz ]
[BG05] B. Barras and B. Grégoire. On the role of type decorations in the calculus of inductive constructions. In L. Ong, editor, Proceedings of CSL'05, volume 3634 of Lecture Notes in Computer Science, pages 151-166, Oxford, UK, August 2005. Springer-Verlag. [ bib | .ps.gz ]
[BGP05] G. Barthe, B. Grégoire, and F. Pastawski. Practical inference for typed-based termination in a polymorphic setting. In P. Urzyczyn, editor, Proceedings of TLCA'05, volume 3641 of Lecture Notes in Computer Science, pages 71-85, Nara, Japan, April 2005. Springer-Verlag. [ bib | .ps.gz ]
[HT05] M. Huisman and K. Trentelman. Factorising temporal specifications. In M. Atkinson and F. Dehne, editors, Proceedings of CATS'05, volume 41 of Conferences in Research and Practice in Information Technology, pages 87-96, Newcastle, Australia, February 2005. ACSC. An earlier version appeared as INRIA Technical Report, nr. RR-5326. [ bib | .ps.gz ]
[Zan05] S. Zanella Béguelin. Formalisation and verification of the GlobalPlatform Card Specification using the B method. In G. Barthe, B. Grégoire, M. Huisman, and J.-L. Lanet, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11 2005, volume 3956 of Lecture Notes in Computer Science, pages 155-173. Springer-Verlag, 2005. [ bib | http ]
[BD05] G. Barthe and G. Dufay. Formal methods for smartcard security. In A. Aldini, R. Gorrieri, and F. Martinelli, editors, Proceedings of FOSAD'05, volume 3655 of Lecture Notes in Computer Science, pages 133-177. Springer-Verlag, 2005. [ bib | .pdf ]
[BRS05] G. Barthe, T. Rezk, and A. Saabas. Proof obligations preserving compilation. In R. Gorrieri, F. Martinelli, P. Ryan, and S. Schneider, editors, Proceedings of FAST'05, volume 3866 of Lecture Notes in Computer Science, pages 112-126. Springer-Verlag, 2005. [ bib | .pdf ]
[Tar05] S. Tarento. Machine-checked security proofs of cryptographic signature schemes. In S. De Capitani di Vimercati, P.F. Syverson, and D. Gollmann, editors, Proceedings of ESORICS'05, volume 3679 of Lecture Notes in Computer Science, pages 140-158. Springer-Verlag, 2005. [ bib | .pdf ]
[BT05] G. Barthe and S. Tarento. A machine-checked formalization of the random oracle model. In J.C. Filliâtre, C. Paulin-Mohring, and B. Werner, editors, Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer Science. Springer-Verlag, 2005. [ bib | .pdf ]
[BRW05] G. Barthe, T. Rezk, and M. Warnier. Preventing timing leaks through transactional branching instructions. In Proceedings of 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL'05), Edinburgh, Scotland, 2005. Electronic Notes in Theoretical Computer Science. to appear. [ bib | .pdf ]
[BR05] G. Barthe and T. Rezk. Non-interference for a JVM-like language. In M. Fähndrich, editor, Proceedings of TLDI'05, pages 103-112, Long Beach, USA, January 2005. ACM Press. [ bib | .ps.gz ]
[BGL05] Y. Bertot, B. Grégoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In J.C. Filliâtre, C. Paulin-Mohring, and B. Werner, editors, Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer Science, pages 66 - 81. Springer-Verlag, 2005. [ bib | .ps.gz ]
[Bar05] G. Barthe. Type isomorphisms and back-and-forth coercions in type theory. Mathematical Structures in Computer Science, 2005. [ bib ]
[BCHJ05] C. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. Formal methods for smart cards: an experience report. Science of Computer Programming, 55(1-3):53-80, 2005. [ bib | .pdf ]
[Cha05] J. Charles. Vérification d'un composant Java: Le vérificateur de bytecode. Master's thesis, Université de Nice, 2005. [ bib | .pdf | .ps ]
[BPN04] G. Barthe and L. Prensa-Nieto. Formally verifying information flow type systems for concurrent and thread systems. In M. Backes, D. Basin, and M. Waidner, editors, Proceedings of FMSE'04, pages 13-22, Washington D.C., USA, October 2004. ACM Press. [ bib | .ps.gz ]
[PBB+04] M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. In P. Paradinas and J.-J. Quisquater, editors, Proceedings of CARDIS'04, Toulouse, France, August 2004. Kluwer Academic Publishers. [ bib | .pdf ]
[BCT04] G. Barthe, J. Cederquist, and S. Tarento. A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin and M. Rusinowitch, editors, Proceedings of IJCAR'04, volume 3097 of Lecture Notes in Computer Science, pages 385-399, Cork, Ireland, July 2004. Springer-Verlag. [ bib | .ps.gz ]
[BDR04] G. Barthe, P. D'Argenio, and T. Rezk. Secure Information Flow by Self-Composition. In R. Foccardi, editor, Proceedings of CSFW'04, pages 100-114, Pacific Grove,USA, June 2004. IEEE Press. [ bib | .ps.gz ]
[BD04] G. Barthe and G. Dufay. A Tool-Assisted Framework for Certified Bytecode Verification. In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages 99-113, Barcelona, Spain, March 2004. Springer-Verlag. [ bib | .ps.gz ]
[HGSC04] M. Huisman, D. Gurov, C. Sprenger, and G. Chugunov. Checking absence of illicit applet interactions: a case study. In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages 84-98, Barcelona, Spain, March 2004. Springer-Verlag. [ bib | .ps.gz ]
[BC04] G. Barthe and T. Coquand. On the equational theory of non-normalizing pure type systems. Journal of Functional Programming, 14(2):191-209, March 2004. [ bib | .ps.gz ]
[BFG+04] G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 14:97-141, February 2004. [ bib | .ps.gz ]
[SGH04] C. Sprenger, D. Gurov, and M. Huisman. Compositional verification for secure loading of smart card applets. In C. Heitmeyer and J.-P. Talpin, editors, Memocode'04, pages 211-222. IEEE Computer Society, 2004. An earlier version appeared as INRIA Technical Report RR-4890. [ bib | .ps.gz ]
[BBR04] G. Barthe, A. Basu, and T. Rezk. Security types preserving compilation. In B. Steffen and G. Levi, editors, Proceedings of VMCAI'04, volume 2934 of Lecture Notes in Computer Science, pages 2-15, Venice, Italy, January 2004. Springer-Verlag. [ bib | .ps.gz ]
[Bar04] G. Barthe. De la théorie des types à la vérification formelles des petits objets portables de sécurité. Habilitation à diriger des recherches, Université de Nice Sophia-Antipolis, 2004. [ bib ]
[Lan04] J.-L. Lanet. Produire des logiciels sûrs. Habilitation à diriger des recherches, Université de Marseille, 2004. [ bib ]
[Cat04] N. Cataño. Formal methods for Java Programs. PhD thesis, Université de Paris, 2004. [ bib ]
[BGH+04] F. Bellegarde, J. Groslambert, M. Huisman, O. Kouchnarenko, and J. Julliand. Verification of liveness properties with JML. Technical Report RR-5331, INRIA, 2004. [ bib | .ps.gz ]
[GH04] D. Gurov and M. Huisman. Abstraction over public interfaces. Technical Report RR-5330, INRIA, 2004. [ bib | .ps.gz ]
[Duf03] G. Dufay. Vérification formelle de la plate-forme Java Card. PhD thesis, Université de Nice Sophia-Antipolis, December 2003. [ bib | .pdf | http ]
[BCC+03] L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of jml tools and applications. In T. Arts and W. Fokkink, editors, FMICS: Eighth International Workshop on Formal Methods for Industrial Critical Systems, volume 80 of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, June 5-7 2003. [ bib | .ps.gz ]
[Cat03] N. Cataño. Slicing event spaces: Towards a Java programs checking framework. In T. Arts and W. Fokkink, editors, FMICS: Eighth International Workshop on Formal Methods for Industrial Critical Systems, volume 80 of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, June 5-7 2003. [ bib ]
[BS03] G. Barthe and S. Stratulat. Using Implicit Induction Techniques for the Validation of the JavaCard Platform. In R. Nieuwenhuis, editor, Proceedings of RTA'03, volume 2706 of Lecture Notes in Computer Science, pages 337 - 351, Valencia, Spain, June 2003. Springer-Verlag. [ bib | .ps.gz ]
[dS03] S. Melo de Sousa. Outils et techniques pour la vérification formelle de la plate-forme JavaCard. PhD thesis, INRIA/Universidade de Nice-Sophia Antipolis, February 2003. [ bib | .ps ]
[CH03] N. Cataño and M. Huisman. Chase: A static checker for JML's assignable clause. In L. D. Zuck, P. C. Attie, A. Cortesi, and S. Mukhopadhyay, editors, VMCAI: Verification, Model Checking and Abstract Interpretation, volume 2575 of Lecture Notes in Computer Science, pages 26-40. Springer-Verlag, January 9-11 2003. [ bib | .ps.gz ]
[BRL03] L. Burdy, A. Requet, and J.-L. Lanet. Java applet correctness: A developer-oriented approach. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME 2003: Formal Methods: International Symposium of Formal Methods Europe, volume 2805 of Lecture Notes in Computer Science, pages 422-439. Springer-Verlag, 2003. [ bib | .ps.gz ]
[BR03] L. Burdy and A. Requet. Extending B with control flow breaks. In D. Bert, J.P. Bowen, S. King, and M. Waldén, editors, ZB 2003: Formal Specification and Development in Z and B, volume 2651 of Lecture Notes in Computer Science, pages 513-527. Springer-Verlag, 2003. [ bib | .ps.gz ]
[BCKL03] G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori. Pure pattern type systems. In Proceedings of POPL'03, New Orleans, USA, January 2003. ACM Press. [ bib | .ps.gz ]
[BCR03] L. Burdy, L. Casset, and A. Requet. Développement d'un vérifieur de byte-code embarqué. Technique et Science Informatiques, 22(1):33-60, 2003. [ bib | .ps.gz ]
[Tar03] S. Tarento. Certifying cryptographic algorithms using the coq system. Rapport de dea, Université de Nice, 2003. [ bib | .dvi ]
[Pav03] M. Pavlova. Automatic generation of jml specification for java card applications. Rapport de dea, Université Paris VII - Denis Diderot, 2003. [ bib | .pdf ]
[BCHJ03] C. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. Formal Methods for Smart Cards: an experience report. Technical Report NIII-R0316, NIII, 2003. [ bib | .html ]
[SGH03] C. Sprenger, D. Gurov, and M. Huisman. Simulation logic, applets and compositional verification. Technical Report RR-4890, INRIA, 2003. [ bib | .ps.gz ]
[PBB+03] M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. Technical Report RR-5061, INRIA, 2003. [ bib | .html ]
[CH02] N. Cataño and M. Huisman. Formal specification of Gemplus' electronic purse case study using ESC/Java. In L.-H. Eriksson and P. Lindsay, editors, FME 2002: Formal Methods: International Symposium of Formal Methods Europe, volume 2391 of Lecture Notes in Computer Science, pages 272-289, Copenhagen, Denmark, July 2002. Springer-Verlag. [ bib | .ps.gz ]
[BGH02] G. Barthe, D. Gurov, and M. Huisman. Compositional verification of secure applet interactions. In Fundamental Approaches to Software Engineering (FASE'02), volume 2306 of Lecture Notes in Computer Science, pages 15-32. Springer-Verlag, 2002. [ bib | .ps.gz ]
[TH02] K. Trentelman and M. Huisman. Extending JML specifications with temporal logic. In H. Kirchner and C. Ringessein, editors, Proceedings of AMAST'02, volume 2422 of Lecture Notes in Computer Science, pages 334-348. Springer-Verlag, 2002. [ bib | .ps.gz ]
[Duf00] G. Dufay. Formalisation en coq de la machine virtuelle javacard. Rapport de dea, Université Paris VII - Denis Diderot, 2000. [ bib | .ps.gz ]
[BCDdS0x] G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Jakarta: tool-assisted specification and verification of the JavaCard Platform. Journal of Automated Reasoning, 200x. To appear. [ bib ]
[BRB0x] G. Barthe, T. Rezk, and A. Basu. Security types preserving compilation. Journal of Computer Languages, Systems and Structures, 200x. To appear. [ bib | .pdf ]

This file has been generated by bibtex2html 1.87.

on Tue, 02 Sep 2008 00:00:10 +0200