english version Toutes les publications de l'équipe
Conference papers
[Format BibTeX]

[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 ]
[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 ]
[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 ]
[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 ]
[BNR06] 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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]

This file has been generated by bibtex2html 1.87.

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