Publications

De CeProMi.

Sommaire 1 Articles en revues avec comité de lecture 2 Articles dans actes de conférences avec comité de lecture 3 Articles en cours de soumission 4 Thèses et mémoires de Master 5 Documents d'enseignement 6 Autres publications

Articles en revues avec comité de lecture

• [completer ici]

Articles dans actes de conférences avec comité de lecture

• Romain Bardou. Ownership, pointer arithmetic and memory separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [1]
• Arthur Charguéraud et François Pottier. Functional translation of a calculus of capabilities. In Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP'08), pages 213-224, septembre 2008.
• Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction, MPC 2008, volume 5133 of Lecture Notes in Computer Science, pages 305-335, Marseille, France, July 2008. Springer.
• Johannes Kanig and Jean-Christophe Filliâtre. Who: A Verifier for Effectful Higher-order Programs. In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009. [2]
• Jean-Christophe Filliâtre. A Functional Implementation of the Garsia-Wachs Algorithm. In ACM SIGPLAN Workshop on ML, Victoria, British Columbia, Canada, September 2008. ACM. [3]
• François Pottier. Hiding local state in direct style: a higher-order anti-frame rule. In Twenty-Third Annual IEEE Symposium on Logic In Computer Science (LICS'08), pages 331-340, Pittsburgh, Pennsylvania, juin 2008.
• [completer ici]

Articles en cours de soumission

• Alexandre Pilkiewicz et François Pottier. The essence of monotonic state. Soumis, juillet 2009.
• Romain Bardou et Claude Marché. Regions and Permissions for Data invariants. Soumis, juillet 2009. Media:bardou09reg.pdf
• Yannick Moy and Claude Marché. Modular Inference of Subprogram Contracts. Soumis à revue JSC, septembre 2009. Media:moy09infer.pdf
• Arthur Charguéraud. Formal Software Verification Through Characteristic Formulae. Soumis, octobre 2009.
• Wendi Urribarri and Christine Paulin-Mohring. Modules and Refinement in Why. Soumis, octobre 2009. Media:urribarri09refin.pdf
• Asma Tafat and Sylvain Boulme and Claude Marche. A Refinement Methodology for Object-Oriented Programs. Soumis, octobre 2009. Media:tafat09refin.pdf
• Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko. Specifying Generic Java Programs: two Case Studies. Soumis à la conférence JFLA 2010, octobre 2010. Media:giorgetti.pdf
• Francois Pottier. Lazy Least Fixed Points in ML. Soumis. PDF

Thèses et mémoires de Master

• Thierry Hubert. Analyse Statique et preuve de Programmes Industriels Critiques. Thèse de doctorat, Université Paris-Sud, June 2008.[4]
• Nicolas Rousset. Automatisation de la Spécification et de la Vérification d'applications Java Card. Thèse de doctorat, Université Paris-Sud, June 2008. [5]
• Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [6]
• Asma Tafat. Invariants et Raffinement en présence de Partage. Mémoire de Master. INRIA & Université Paris 6. Septembre 2009. [7]
• Elena Tushkanova. Modular Specification of Object-Oriented Programs. Master Report. Yaroslavl State University, Russia. June 2009.
• A venir: Wendi Urribarri. These de doctorat, Université Paris-Sud, 2009.
• [completer ici]

Documents d'enseignement

• Claude Marché, Notes de cours sur Krakatoa (Ecole d'hiver du COST FVOOS)

Autres publications

• Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. [8].
• Elena Tushkanova, Alain Giorgetti, Olga Kouchnarenko. Specifying and Proving a Sorting Algorithm. LIFC research report RR2009-03, 35 pages. October 2009.
• Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko. Modular Specification of Generic Java Programs. INRIA research report. December 2009.[completer ici]