EN FR
EN FR




Bibliography

Major publications by the team in recent years
  • 1S. Boldo.

    Floats & Ropes: a case study for formal numerical program verification, in: 36th International Colloquium on Automata, Languages and Programming, Rhodos, Greece, Lecture Notes in Computer Science - ARCoSS, Springer, July 2009, vol. 5556, p. 91–102.
  • 2S. Boldo, J.-C. Filliâtre.

    Formal Verification of Floating-Point Programs, in: 18th IEEE International Symposium on Computer Arithmetic, Montpellier, France, June 2007, p. 187-194.

    http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf
  • 3S. Conchon, É. Contejean, J. Kanig, S. Lescuyer.

    CC(X): Semantical Combination of Congruence Closure with Solvable Theories, in: Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Electronic Notes in Computer Science, Elsevier Science Publishers, 2008, vol. 198-2, p. 51–69.
  • 4É. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain.

    Certification of automated termination proofs, in: 6th International Symposium on Frontiers of Combining Systems (FroCos 07), Liverpool,UK, B. Konev, F. Wolter (editors), Lecture Notes in Artificial Intelligence, Springer, September 2007, vol. 4720, p. 148–162.
  • 5É. Contejean, C. Marché, A. P. Tomás, X. Urbain.

    Mechanically proving termination using polynomial interpretations, in: Journal of Automated Reasoning, 2005, vol. 34, no 4, p. 325–363.

    http://dx.doi.org/10.1007/s10817-005-9022-x
  • 6J.-C. Filliâtre.

    Verification of Non-Functional Programs using Interpretations in Type Theory, in: Journal of Functional Programming, July 2003, vol. 13, no 4, p. 709–745.

    http://www.lri.fr/~filliatr/ftp/publis/jphd.pdf
  • 7J.-C. Filliâtre, C. Marché.

    Multi-Prover Verification of C Programs, in: 6th International Conference on Formal Engineering Methods, Seattle, WA, USA, J. Davies, W. Schulte, M. Barnett (editors), Lecture Notes in Computer Science, Springer, November 2004, vol. 3308, p. 15–29.

    http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz
  • 8T. Hubert, C. Marché.

    A case study of C source code verification: the Schorr-Waite algorithm, in: 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, B. K. Aichernig, B. Beckert (editors), IEEE Comp. Soc. Press, September 2005.

    http://www.lri.fr/~marche/hubert05sefm.ps
  • 9S. Krstić, S. Conchon.

    Canonization for disjoint unions of theories, in: Information and Computation, May 2005, vol. 199, no 1-2, p. 87–106.
  • 10C. Marché, C. Paulin-Mohring, X. Urbain.

    The Krakatoa Tool for Certification of Java/JavaCard Programs annotated in JML , in: Journal of Logic and Algebraic Programming, 2004, vol. 58, no 1–2, p. 89–106.

    http://krakatoa.lri.fr
Publications of the year

Doctoral Dissertations and Habilitation Theses

  • 11R. Bardou.

    Verification of Pointer Programs Using Regions and Permissions, Université Paris-Sud, October 2011.

    http://romain.bardou.fr/thesis/bardou11phd.pdf
  • 12F. Bobot.

    Logique de séparation et vérification déductive, Université Paris-Sud, December 2011.
  • 13J.-C. Filliâtre.

    Deductive Program Verification, Université Paris-Sud, December 2011, Thèse d'habilitation.
  • 14S. Lescuyer.

    Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq, Université Paris-Sud, January 2011.

Articles in International Peer-Reviewed Journal

  • 15S. Boldo, C. Marché.

    Formal verification of numerical programs: from C annotated programs to mechanical proofs, in: Mathematics in Computer Science, 2011.
  • 16S. Boldo, J.-M. Muller.

    Exact and Approximated error of the FMA, in: IEEE Transactions on Computers, February 2011, vol. 60, no 2, p. 157–164.

    http://hal.inria.fr/inria-00429617/en/
  • 17S. Boldo, T. M. T. Nguyen.

    Proofs of numerical programs when the compiler optimizes, in: Innovations in Systems and Software Engineering, 2011, vol. 7, p. 151-160.
  • 18J.-C. Filliâtre.

    Deductive Software Verification, in: International Journal on Software Tools for Technology Transfer (STTT), August 2011, vol. 13, no 5, p. 397-403.

    http://dx.doi.org/10.1007/s10009-011-0211-0
  • 19F. de Dinechin, C. Lauter, G. Melquiond.

    Certifying the floating-point implementation of an elementary function using Gappa, in: IEEE Transactions on Computers, 2011, vol. 60, no 2, p. 242–253.

    http://hal.inria.fr/inria-00533968/en/

International Conferences with Proceedings

  • 20D. Baelde, R. Beauxis, S. Mimram.

    Liquidsoap: A High-Level Programming Language for Multimedia Streaming, in: 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11), Nový Smokovec, Slovakia, I. Cerná, T. Gyimóthy, J. Hromkovic, K. G. Jeffery, R. Královic, M. Vukolic, S. Wolf (editors), Lecture Notes in Computer Science, Springer, January 2011, vol. 6543.
  • 21F. Bobot, J.-C. Filliâtre, C. Marché, A. Paskevich.

    Why3: Shepherd Your Herd of Provers, in: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wrocław, Poland, August 2011.

    http://proval.lri.fr/submissions/boogie11.pdf
  • 22F. Bobot, A. Paskevich.

    Expressing Polymorphic Types in a Many-Sorted Language, in: Frontiers of Combining Systems, 8th International Symposium, Proceedings, Saarbrücken, Germany, C. Tinelli, V. Sofronie-Stokkermans (editors), Lecture Notes in Computer Science, October 2011, vol. 6989.
  • 23S. Boldo, G. Melquiond.

    Flocq: A Unified Library for Proving Floating-point Algorithms in Coq, in: Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Tübingen, Germany, E. Antelo, D. Hough, P. Ienne (editors), 2011, p. 243–252.

    http://www.lri.fr/~melquion/doc/11-arith20-article.pdf
  • 25É. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain.

    Automated Certified Proofs with CiME3, in: 22nd International Conference on Rewriting Techniques and Applications (RTA 11), Novi Sad, Serbia, M. Schmidt-Schauß (editor), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2011, vol. 10, p. 21–30.

    http://drops.dagstuhl.de/opus/volltexte/2011/3119
  • 26C. Dross, J.-C. Filliâtre, Y. Moy.

    Correct Code Containing Containers, in: 5th International Conference on Tests and Proofs (TAP'11), Zurich, June 2011.
  • 27J.-C. Filliâtre, K. Kalyanasundaram.

    Functory: A Distributed Computing Library for Objective Caml, in: Trends in Functional Programming, Madrid, Spain, May 2011.
  • 28T. M. T. Nguyen, C. Marché.

    Hardware-Dependent Proofs of Numerical Programs, in: Certified Programs and Proofs, J.-P. Jouannaud, Z. Shao (editors), Lecture Notes in Computer Science, Springer, December 2011.
  • 29A. Tafat, S. Boulmé, C. Marché.

    A Refinement Methodology for Object-Oriented Programs, in: Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, B. Beckert, C. Marché (editors), Lecture Notes in Computer Science, Springer, January 2011, vol. 6528, p. 153–167.

National Conferences with Proceeding

  • 30R. Bardou, C. Marché.

    Perle de preuve: les tableaux creux, in: Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, S. Conchon (editor), INRIA, January 2011.
  • 31J.-C. Filliâtre, K. Kalyanasundaram.

    Une bibliothèque de calcul distribué pour Objective Caml, in: Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, S. Conchon (editor), INRIA, January 2011.

    http://www.lri.fr/~filliatr/publis/jfla-2011.pdf

Scientific Books (or Scientific Book chapters)

  • 32S. Boldo, T. Viéville.

    Représentation numérique de l'information, in: Introduction à la science informatique, G. Dowek (editor), Repères pour agir, CRDP Académie de Paris, July 2011, p. 23–72.

    http://crdp.ac-paris.fr/Introduction-a-la-science
  • 33S. Boldo, T. Viéville.

    Structuration et contrôle de l'information, in: Introduction à la science informatique, G. Dowek (editor), Repères pour agir, CRDP Académie de Paris, July 2011, p. 281–308.

    http://crdp.ac-paris.fr/Introduction-a-la-science

Books or Proceedings Editing

  • 34B. Beckert, C. Marché (editors)

    Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, Lecture Notes in Computer Science, Springer, January 2011, vol. 6528.

Internal Reports

Other Publications

  • 42F. Bobot, A. Paskevich.

    Expressing Polymorphic Types in a Many-Sorted Language, 2011.
  • 43N. Gaspar.

    Mechanized Semantics into Concurrent Program verification, September 2011, http://www.lri.fr/~gaspar/rgcoq.html.
  • 44C. Lelay.

    Étude de la différentiabilité et de l'intégrabilité en Coq : Application à la formule de d'Alembert pour l'équation des ondes, Université Paris 7, 2011.
References in notes
  • 45The MAUDE System.
  • 46J. Andronick.

    Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocessur. Plateforme Java Card et Système d'exploitation, Université Paris-Sud, March 2006.

    http://ssrg.nicta.com.au/publications/papers/Andronick:phd.abstract?bib=login
  • 47J. Andronick, B. Chetali, C. Paulin-Mohring.

    Formal Verification of Security Properties of Smart Card Embedded Source Code, in: International Symposium of Formal Methods Europe (FM'05), Newcastle,UK, J. Fitzgerald, I. J. Hayes, A. Tarlecki (editors), Lecture Notes in Computer Science, Springer, July 2005, vol. 3582.

    http://www.springerlink.com/content/eulj9pbgm2875cer/
  • 48T. Arts, J. Giesl.

    Termination of term rewriting using dependency pairs, in: Theoretical Computer Science, 2000, vol. 236, p. 133–178.
  • 49P. Audebaud, C. Paulin-Mohring.

    Proofs of Randomized Algorithms in Coq, in: Science of Computer Programming, 2009, vol. 74, no 8, p. 568–589.

    http://hal.inria.fr/inria-00431771/en/
  • 50M. Barbosa, J.-C. Filliâtre, J. S. Pinto, B. Vieira.

    A Deductive Verification Platform for Cryptographic Software, in: 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), Pisa, Italy, Electronic Communications of the EASST, September 2010, vol. 33.

    http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461
  • 51R. Bardou, J.-C. Filliâtre, J. Kanig, S. Lescuyer.

    Faire bonne figure avec Mlpost, in: Vingtièmes Journées Francophones des Langages Applicatifs, Saint-Quentin sur Isère, INRIA, January 2009.

    http://www.lri.fr/~filliatr/ftp/publis/mlpost-fra.pdf
  • 52B. Barras.

    Verification of the Interface of a Small Proof System in Coq, in: Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers, E. Giménez, C. Paulin-Mohring (editors), Lecture Notes in Computer Science, Springer, 1998, vol. 1512, p. 28-45.
  • 53G. Barthe, B. Grégoire, S. Z. Béguelin.

    Formal certification of code-based cryptographic proofs, in: POPL, Savannah, GA, USA, Z. Shao, B. C. Pierce (editors), ACM Press, January 2009, p. 90-101.
  • 54P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, V. Prevosto.

    ACSL: ANSI/ISO C Specification Language, version 1.4, 2009.

    http://frama-c.cea.fr/acsl.html
  • 55S. Boldo.

    Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms, in: Third International Joint Conference on Automated Reasoning, Seattle, USA, U. Furbach, N. Shankar (editors), Lecture Notes in Computer Science, Springer, August 2006, vol. 4130, p. 52-66.

    http://www.springerlink.com/content/524v5246177t0877/
  • 56S. Boldo.

    Floats & Ropes: a case study for formal numerical program verification, in: 36th International Colloquium on Automata, Languages and Programming, Rhodos, Greece, Lecture Notes in Computer Science - ARCoSS, Springer, July 2009, vol. 5556, p. 91–102.
  • 57S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, P. Weis.

    Formal Proof of a Wave Equation Resolution Scheme: the Method Error, in: Proceedings of the first Interactive Theorem Proving Conference, Edinburgh, Scotland, M. Kaufmann, L. C. Paulson (editors), LNCS, Springer, July 2010, vol. 6172, p. 147–162.

    http://hal.inria.fr/inria-00450789/en/
  • 58R. Bornat.

    Proving Pointer Programs in Hoare Logic, in: Mathematics of Program Construction, 2000, p. 102–126.
  • 59V. Chaudhary.

    The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A Case Study, IIT internship report, July 2004.
  • 60S. Conchon, S. Krstić.

    Strategies for Combining Decision Procedures, in: Theoretical Computer Science, 2006, vol. 354, no 2, p. 187–210.
  • 61É. Contejean, P. Corbineau.

    Reflecting Proofs in First-Order Logic with Equality, in: 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, R. Nieuwenhuis (editor), Lecture Notes in Artificial Intelligence, Springer, July 2005, vol. 3632, p. 7–22.
  • 62É. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain.

    Certification of automated termination proofs, CEDRIC, May 2007, no 1185.
  • 63É. Contejean, C. Marché, A. P. Tomás, X. Urbain.

    Mechanically proving termination using polynomial interpretations, in: Journal of Automated Reasoning, 2005, vol. 34, no 4, p. 325–363.

    http://dx.doi.org/10.1007/s10817-005-9022-x
  • 64J.-F. Couchot, A. Giorgetti, N. Stouls.

    Graph-based Reduction of Program Verification Conditions, INRIA Saclay – Île-de-France, October 2008, no 6702.

    http://hal.inria.fr/inria-00339847/en/
  • 65J.-F. Couchot, S. Lescuyer.

    Handling Polymorphism in Automated Deduction, in: 21th International Conference on Automated Deduction (CADE-21), Bremen, Germany, LNCS (LNAI), July 2007, vol. 4603, p. 263–278.
  • 66M. Daumas, G. Melquiond.

    Certification of bounds on expressions involving rounded operators, in: Transactions on Mathematical Software, 2010, vol. 37, no 1.

    http://hal.archives-ouvertes.fr/inria-00534350/fr/
  • 67F. Durán, S. Lucas, J. Meseguer, C. Marché, X. Urbain.

    Proving Termination of Membership Equational Programs, in: ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, ACM Press, August 2004.
  • 68J.-C. Filliâtre.

    Formal Proof of a Program: Find, in: Science of Computer Programming, 2006, vol. 64, p. 332–240.

    http://www.lri.fr/~filliatr/ftp/publis/find.pdf
  • 69J.-C. Filliâtre.

    Verifying Two Lines of C with Why3: an Exercise in Program Verification, in: Verified Software: Theories, Tools and Experiments (VSTTE), Philadelphia, USA, January 2012.

    http://why3.lri.fr/queens/queens.pdf
  • 70J.-C. Filliâtre, S. Owre, H. Rueß, N. Shankar.

    ICS: Integrated Canonization and Solving (Tool presentation), in: Proceedings of CAV'2001, G. Berry, H. Comon, A. Finkel (editors), Lecture Notes in Computer Science, Springer, 2001, vol. 2102, p. 246–249.
  • 71J. Gerlach, J. Burghardt.

    An Experience Report on the Verification of Algorithms in the C++ Standard Library using Frama-C, in: Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Paris, France, B. Beckert, C. Marché (editors), Karlsruhe Reports in Informatics, June 2010, p. 191–204.
  • 72B. Gramlich.

    On Proving Termination by Innermost Termination, in: 7th International Conference on Rewriting Techniques and Applications, New Brunswick, NJ, USA, H. Ganzinger (editor), Lecture Notes in Computer Science, Springer, July 1996, vol. 1103, p. 93–107.
  • 73T. Hubert.

    Analyse Statique et preuve de Programmes Industriels Critiques, Université Paris-Sud, June 2008.

    http://www.lri.fr/~marche/hubert08these.pdf
  • 74T. Hubert, C. Marché.

    Separation Analysis for Deductive Verification, in: Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007, p. 81–93.

    http://www.lri.fr/~marche/hubert07hav.pdf
  • 75B. Jacobs, C. Marché, N. Rauch.

    Formal Verification of a Commercial Smart Card Applet with Multiple Tools, in: Algebraic Methodology and Software Technology, Stirling, UK, Lecture Notes in Computer Science, Springer, July 2004, vol. 3116.
  • 76K. R. M. Leino, M. Moskal.

    VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0, in: Proceedings of Tools and Experiments Workshop at VSTTE, 2010.
  • 77C. Lelay, G. Melquiond.

    Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert, in: Vingt-troisièmes Journées Francophones des Langages Applicatifs, Carnac, France, February 2012.

    http://hal.inria.fr/hal-00642206/fr/
  • 78X. Leroy.

    Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, in: Conference Record of the 33rd Symposium on Principles of Programming Languages, Charleston, South Carolina, ACM Press, January 2006.
  • 79S. Lescuyer.

    Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes, Master Parisien de Recherche en Informatique, 2006.
  • 80P. Letouzey.

    A New Extraction for Coq, in: TYPES 2002, H. Geuvers, F. Wiedijk (editors), Lecture Notes in Computer Science, Springer, 2003, vol. 2646.
  • 81P. Letouzey.

    Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq, Université Paris-Sud, July 2004.
  • 82C. Marché, C. Paulin-Mohring.

    Reasoning about Java Programs with Aliasing and Frame Conditions, in: 18th International Conference on Theorem Proving in Higher Order Logics, J. Hurd, T. Melham (editors), Lecture Notes in Computer Science, Springer, August 2005, vol. 3603, p. 179–194.

    http://www.lri.fr/~marche/marche05tphols.ps
  • 83C. Marché, N. Rousset.

    Verification of Java Card Applets Behavior with respect to Transactions and Card Tears, in: 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, D. V. Hung, P. Pandya (editors), IEEE Comp. Soc. Press, September 2006.
  • 84C. Marché, X. Urbain.

    Modular and Incremental Proofs of AC-Termination, in: Journal of Symbolic Computation, 2004, vol. 38, p. 873–897.

    http://authors.elsevier.com/sd/article/S074771710400029X
  • 85C. Marché.

    Preuves mécanisées de Propriétés de Programmes, Université Paris 11, December 2005, Thèse d'habilitation.
  • 86G. Melquiond, W. G. Nowak, P. Zimmermann.

    Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819..., in: Mathematics of Computation, 2012.

    http://hal.inria.fr/hal-00644166/en/
  • 87Y. Moy, C. Marché.

    Modular Inference of Subprogram Contracts for Safety Checking, in: Journal of Symbolic Computation, 2010, vol. 45, p. 1184-1211.

    http://hal.inria.fr/inria-00534331/en/
  • 88Y. Moy.

    Automatic Modular Static Safety Checking for C Programs, Université Paris-Sud, January 2009.

    http://www.lri.fr/~marche/moy09phd.pdf
  • 89E. Ohlebusch, C. Claves, C. Marché.

    TALP: A Tool for the Termination Analysis of Logic Programs, in: 11th International Conference on Rewriting Techniques and Applications, Norwich, UK, L. Bachmair (editor), Lecture Notes in Computer Science, Springer, July 2000, vol. 1833, p. 270–273.
  • 90S. Ranise, C. Tinelli.

    The Satisfiability Modulo Theories Library (SMT-LIB), 2006, http://www.smtcomp.org.
  • 91M. Sozeau.

    Program-ing Finger Trees in Coq, in: 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, R. Hinze, N. Ramsey (editors), ACM Press, 2007, p. 13–24.
  • 92M. Sozeau.

    Un environnement pour la programmation avec types dépendants, Université Paris-Sud, December 2008.
  • 93D. Stevenson.

    A proposed standard for binary floating point arithmetic, in: IEEE Computer, 1981, vol. 14, no 3, p. 51-62.
  • 94X. Urbain.

    Approche incrémentale des preuves automatiques de terminaison, Université Paris-Sud, Orsay, France, October 2001.

    http://www.lri.fr/~urbain/textes/these.ps.gz