Wiki Agenda Contact Version française

Publications since 2004

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

  Books and book chapters

[19] Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In Bruno Woltzenlogel Paleo and David Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications, January 2015. [ bib | http | .pdf ]
Keywords: Coq proof assistant ; Calculus of Inductive Constructions
[18] Sylvie Boldo. Même les ordinateurs font des erreurs ! In Martin Andler, Liliane Bel, Sylvie Benzoni-Gavage, Thierry Goudon, Cyril Imbert, and Antoine Rousseau, editors, Brèves de maths, pages 136--137. Nouveau Monde Editions, October 2014. [ bib | full text on HAL | http ]
[17] Sylvain Conchon and Jean-Christophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Eyrolles, September 2014. [ bib | full text on HAL | http ]
[16] Benjamin Wack, Sylvain Conchon, Judicaël Courant, Marc de Falco, Gilles Dowek, Jean-Christophe Filliâtre, and Stéphane Gonnord. Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python. Eyrolles, August 2013. [ bib | full text on HAL | http ]
[15] Sylvie Boldo and Guillaume Melquiond. Informatique Mathématique, une photographie en 2013, chapter Arithmétique des ordinateurs et preuves formelles, pages 189--220. Presses Universitaires de Perpignan, Perpignan, France, 2013. [ bib | full text on HAL ]
[14] Jean-Christophe Filliâtre. Course notes EJCP 2012, chapter Vérification déductive de programmes avec Why3. June 2012. [ bib | http ]
Keywords: Why3
[13] Sylvie Boldo and Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. In Valérie Berthé, Christiane Frougny, Natacha Portier, Marie-Françoise Roy, and Anne Siegel, editors, École des Jeunes Chercheurs en Informatique Mathématique, pages 1--30. Rennes, France, March 2012. [ bib | full text on HAL ]
[12] Christine Paulin-Mohring. Tools for practical software verification (international summer school, LASER 2011, revised tutorial lectures). volume 7682 of Lecture Notes in Computer Science, chapter Introduction to the Coq proof-assistant for practical software verification. Springer, 2012. [ bib | .pdf ]
[11] Sylvie Boldo and Thierry Viéville. Représentation numérique de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 23--72. CRDP Académie de Paris, July 2011. [ bib | http ]
[10] Sylvie Boldo and Thierry Viéville. Structuration et contrôle de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 281--308. CRDP Académie de Paris, July 2011. [ bib | http ]
[9] Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010. [ bib ]
[8] V. Benzaken, G. Castagna, H. Hosoya, B.C. Pierce, and S. Vansummeren. The Encyclopedia of Database Systems, chapter “XML Typechecking”. Springer, 2009. Invited Article. [ bib ]
[7] Christine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. In Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin, editors, From Semantics to Computer Science: Essays in Honor of Gilles Kahn. Cambridge University Press, 2009. [ bib | full text on HAL | PDF ]
[6] Sylvie Boldo. Demandez le programme! In DocSciences, volume 5, pages 26--33. C.R.D.P. de l'académie de Versailles, November 2008. http://www.docsciences.fr/-DocSciences-no5-. [ bib | http ]
[5] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Marco T. Morazán, editor, Trends in Functional Programming Volume 8: Selected Papers of the 8th International Symposium on Trends in Functional Programming (TFP'07), New York, USA, volume 8. Intellect, 2008. [ bib ]
[4] Paul Caspi, Grégoire Hamon, and Marc Pouzet. Real-Time Systems: Models and verification --- Theory and tools, chapter Synchronous Functional Programming with Lucid Synchrone. ISTE, 2007. [ bib ]
[3] Évelyne Contejean. Modelling permutations in Coq for Coccinelle. In Hubert Comon-Lundth, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 259--269. Springer, 2007. Jouannaud Festschrift. [ bib | DOI | Abstract ]
[2] Claude Marché. Towards modular algebraic specifications for pointer programs: a case study. In Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235--258. Springer, 2007. [ bib ]
[1] Paul Caspi, Grégoire Hamon, and Marc Pouzet. Systèmes Temps-réel : Techniques de Description et de Vérification -- Théorie et Outils, volume 1, chapter Lucid Synchrone, un langage de programmation des systèmes réactifs, pages 217--260. Hermes, 2006. [ bib ]

  Journals

[51] Sylvie Boldo, Stef Graillat, and Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, 44(1), July 2017. [ bib | full text on HAL | .pdf ]
[50] Martin Clochard, Léon Gondelman, and Mário Pereira. The matrix reproved. Journal of Automated Reasoning, 2017. [ bib | full text on HAL ]
[49] Ran Chen, Martin Clochard, and Claude Marché. A formally proved, complete algorithm for path resolution with symbolic links. Journal of Formalized Reasoning, 10(1):51--66, 2017. [ bib | DOI | full text on HAL | http ]
[48] Umut A Acar, Arthur Charguéraud, and Mike Rainey. Oracle-guided scheduling for controlling granularity in implicitly parallel languages. Journal of Functional Programming, 26, November 2016. [ bib | DOI | full text on HAL ]
[47] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 2016. [ bib | full text on HAL ]
[46] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Adding decision procedures to SMT solvers using axioms with triggers. Journal of Automated Reasoning, 56(4):387--457, 2016. [ bib | full text on HAL ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists.

[45] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. Formal Methods in System Design, 48(3):152--174, 2016. [ bib | DOI | full text on HAL ]
In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this article, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Keywords: Why3
[44] Érik Martin-Dorel and Guillaume Melquiond. Proving tight bounds on univariate expressions with elementary functions in Coq. Journal of Automated Reasoning, 2016. [ bib | DOI | full text on HAL ]
Keywords: Coq proof assistant ; formal proof ; decision procedure ; interval arithmetic ; floating-point arithmetic ; nonlinear arithmetic
[43] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41--62, June 2015. [ bib | DOI | full text on HAL ]
[42] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135--163, February 2015. [ bib | full text on HAL ]
[41] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709--727, 2015. See also http://toccata.lri.fr/gallery/fm2012comp.en.html. [ bib | DOI | full text on HAL ]
[40] Claude Marché and Johannes Kanig. Bridging the gap between testing and formal verification in Ada development. ERCIM News, 100:38--39, January 2015. [ bib | full text on HAL ]
[39] Pierre Roux. Formal proofs of rounding error bounds. Journal of Automated Reasoning, 2015. [ bib | DOI | full text on HAL ]
Keywords: floating-point arithmetic ; rounding error ; numerical analysis ; proof assistant ; Coq ; matrices ; Cholesky decomposition
[38] Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Journal of Automated Reasoning, 54(1):1--29, 2015. [ bib | DOI | full text on HAL ]
Keywords: formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic
[37] Sylvie Boldo and Jean-Michel Muller. Des ordinateurs capables de calculer plus juste. La Recherche, 492:46--52, October 2014. [ bib | full text on HAL ]
[36] Claude Marché. Verification of the functional behavior of a floating-point program: an industrial case study. Science of Computer Programming, 96(3):279--296, March 2014. [ bib | DOI | full text on HAL | .pdf ]
We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving

[35] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325--352, 2014. [ bib | DOI | full text on HAL | http ]
[34] Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Journal of Automated Reasoning, pages 1--29, 2014. [ bib | DOI | full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic
[33] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423--456, April 2013. [ bib | DOI | full text on HAL ]
[32] Véronique Benzaken, Giuseppe Castagna, Dario Colazzo, and Kim Nguyen. Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems (TODS), 2013. [ bib | full text on HAL ]
[31] Guillaume Melquiond, Werner Georg Nowak, and Paul Zimmermann. Numerical approximation of the Masser-Gramain constant to four decimal digits: delta=1.819.... Mathematics of Computation, 82:1235--1246, 2013. [ bib | DOI | full text on HAL ]
[30] Diego Arroyuelo, Francisco Claude, Sebastian Maneth, Veli Mäkinen, Gonzalo Navarro, Kim Nguyen, Jouni Sirén, and Niko Välimäki. Fast in-memory XPath search using compressed indexes. Software: Practice and Experience, pages n/a--n/a, 2013. [ bib | DOI ]
Keywords: XML, succinct data structures, XPath, tree automata
[29] Érik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double roundings. BIT Numerical Mathematics, 53(4):897--924, 2013. [ bib | DOI | full text on HAL ]
[28] José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Science of Computer Programming, October 2012. Accepted for publication. [ bib | DOI ]
[27] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation. Logical Methods in Computer Science, 8(3):1--29, September 2012. Selected Papers of the Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany, 2011. [ bib | DOI | full text on HAL | http ]
[26] Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14--23, 2012. [ bib | DOI | full text on HAL ]
[25] Jean-Christophe Filliâtre. Deductive software verification. International Journal on Software Tools for Technology Transfer (STTT), 13(5):397--403, August 2011. [ bib | DOI | .pdf ]
Deductive software verification, also known as program proving, expresses the correctness of a program as a set of mathematical statements, called verification conditions. They are then discharged using either automated or interactive theorem provers. We briefly review this research area, with an emphasis on tools.

[24] Sylvie Boldo and Jean-Michel Muller. Exact and Approximated error of the FMA. IEEE Transactions on Computers, 60(2):157--164, February 2011. [ bib | full text on HAL ]
The fused multiply accumulate-add (FMA) instruction, specified by the IEEE 754-2008 Standard for Floating-Point Arithmetic, eases some calculations, and is already available on some current processors such as the Power PC or the Itanium. We first extend an earlier work on the computation of the exact error of an FMA (by giving more general conditions and providing a formal proof). Then, we present a new algorithm that computes an approximation to the error of an FMA, and provide error bounds and a formal proof for that algorithm.

[23] Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242--253, 2011. [ bib | DOI | full text on HAL ]
[22] Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, 7:151--160, 2011. [ bib | full text on HAL ]
[21] Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377--393, 2011. [ bib | DOI | full text on HAL | .pdf ]
[20] Marc Pouzet and Pascal Raymond. Modular Static Scheduling of Synchronous Data-flow Networks: An efficient symbolic representation. Journal of Design Automation for Embedded Systems, 2010. Special issue of selected papers from http://esweek09.inrialpes.fr/Embedded System Week. [ bib ]
[19] Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1), 2010. [ bib | DOI | full text on HAL ]
[18] Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184--1211, 2010. [ bib | DOI | full text on HAL ]
[17] Siegfried M. Rump, Paul Zimmermann, Sylvie Boldo, and Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT, 49(2):419--431, June 2009. [ bib | DOI | full text on HAL ]
[16] Sylvie Boldo. Kahan's algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220--225, February 2009. [ bib | DOI | full text on HAL | PDF ]
[15] Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568--589, 2009. [ bib | DOI | full text on HAL | PDF ]
[14] Sylvie Boldo, Marc Daumas, and Ren-Cang Li. Formally verified argument reduction with a fused-multiply-add. IEEE Transactions on Computers, 58(8):1139--1145, 2009. [ bib | DOI | PDF | http ]
[13] Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4):1--64, 2008. [ bib | DOI ]
[12] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1--2):59--88, 2008. [ bib | full text on HAL | PDF | .pdf ]
[11] Louis Mandel and Marc Pouzet. ReactiveML : un langage fonctionnel pour la programmation réactive. Technique et Science Informatiques (TSI), 27(9--10/2008):1097--1128, 2008. [ bib | PDF | .pdf ]
[10] Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and Correctly-Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462--471, 2008. [ bib | DOI | full text on HAL ]
[9] Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. Theoretical Computer Science, 354(2):187--210, 2006. Special Issue of TCS dedicated to a refereed selection of papers presented at TACAS'03. [ bib ]
[8] Jean-Christophe Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332--240, 2006. [ bib | DOI | PDF | .pdf ]
[7] Alain Girault, Xavier Nicollin, and Marc Pouzet. Automatic Rate Desynchronization of Embedded Reactive Programs. ACM Transactions on Embedded Computing Systems (TECS), 5(3), 2006. [ bib ]
[6] Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(1-2):87--106, May 2005. [ bib ]
[5] Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning, 34(4):325--363, 2005. [ bib | DOI | Abstract ]
[4] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446--453, 2005. [ bib ]
We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs

[3] Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873--897, 2004. [ bib | http ]
[2] Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1--2):89--106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ]
[1] Xavier Urbain. Modular and incremental automated termination proofs. Journal of Automated Reasoning, 32:315--355, 2004. [ bib | .ps.gz ]

  Conferences

[230] Florian Faissole and Bas Spitters. Preuves constructives de programmes probabilistes. In Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL ]
[229] Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. In Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]
[228] Raphaël Rieu-Helft. Un mécanisme d'extraction vers C pour Why3. In Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]
[227] Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, and Valentina Popescu. Formal verification of a floating-point expansion renormalization algorithm. In Proceedings of the 8th International Conference on Interactive Theorem Proving, Brasilia, Brazil, September 2017. [ bib | full text on HAL | .pdf ]
[226] Florian Faissole. Formalization and closedness of finite dimensional subspaces. In SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timișoara, Romania, September 2017. [ bib | http | .pdf ]
Keywords: filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq
[225] Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. Springer. [ bib | full text on HAL ]
[224] Nicolas Jeannerod, Claude Marché, and Ralf Treinen. A formally verified interpreter for a shell-like programming language. In Andrei Paskevich and Thomas Wies, editors, 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. Springer. [ bib | full text on HAL ]
[223] Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error analysis of explicit one-step numerical integration methods. In 24th IEEE Symposium on Computer Arithmetic, London, United Kingdom, July 2017. [ bib | DOI | full text on HAL | .pdf ]
[222] Ran Chen and Jean-Jacques Lévy. A semi-automatic proof of strong connectivity. In 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Heidelberg, Germany, July 2017. [ bib | full text on HAL ]
[221] Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond. How to get an efficient yet verified arbitrary-precision integer library. In 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. [ bib | full text on HAL | .pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier
[220] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. Preuve formelle du théorème de Lax--Milgram. In 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ]
[219] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79--89, New York, NY, USA, January 2017. ACM. [ bib | DOI | full text on HAL | .pdf ]
[218] Ran Chen and Jean-Jacques Lévy. Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[217] Martin Clochard. Preuves taillées en biseau. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[216] Mário Pereira. Défonctionnaliser pour prouver. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[215] Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, and Clément Fumex. A three-tier strategy for reasoning about floating-point numbers in SMT. In Computer Aided Verification, 2017. [ bib | full text on HAL ]
[214] Raphaël Rieu-Helft and Pascal Cuoq. Result graphs for an abstract interpretation-based static analyzer. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ]
[213] Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles. Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In Tiziana Margaria and Bernhard Steffen, editors, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 9952 of Lecture Notes in Computer Science, pages 461--478, Corfu, Greece, October 2016. Springer. [ bib | full text on HAL ]
[212] Umut A Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski. Dag-calculus: a calculus for parallel computation. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 18--32, Nara, Japan, September 2016. [ bib | DOI | full text on HAL ]
[211] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, Nancy, France, August 2016. [ bib | DOI | full text on HAL | .pdf ]
[210] Jean-Christophe Filliâtre and Mário Pereira. Producing all ideals of a forest, formally (verification pearl). In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib | full text on HAL ]
[209] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib | full text on HAL ]
[208] Sylvie Boldo. Computing a correct and tight rounding error bound using rounding-to-nearest. In 9th International Workshop on Numerical Software Verification, Toronto, Canada, July 2016. [ bib | full text on HAL | .pdf ]
[207] Sylvie Boldo. Iterators: where folds fail. In Workshop on High-Consequence Control Verification, Toronto, Canada, July 2016. [ bib | full text on HAL | .pdf ]
[206] Jean-Christophe Filliâtre and Mário Pereira. A modular way to reason about iteration. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, Minneapolis, MN, USA, June 2016. Springer. [ bib | full text on HAL ]
In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the nite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with non-deterministic and possibly innite iteration. We show how to cope with the issue of an iteration no longer being consistent with mutable data. We validate our proposal using the deductive verication tool Why3 and two iteration paradigms, namely cursors and higher-order iterators. For each paradigm, we verify several implementations of iterators and client code. This is done in a modular way, i.e., the client code only relies on the specication of the iteration.

[205] Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché. Specification and proof of high-level functional properties of bit-level programs. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, pages 291--306, Minneapolis, MN, USA, June 2016. Springer. [ bib | full text on HAL ]
[204] Jean-Christophe Filliâtre and Mário Pereira. Itérer avec confiance. In Vingt-septièmes Journées Francophones des Langages Applicatifs, Saint-Malo, France, January 2016. [ bib | full text on HAL ]
[203] David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in SPARK. In Rocco De Nicola and Eva Kühn, editors, Software Engineering and Formal Methods, Lecture Notes in Computer Science, pages 215--233, Vienna, Austria, 2016. [ bib | DOI | full text on HAL ]
[202] Arthur Charguéraud. Higher-Order Representation Predicates in Separation Logic. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, Florida, United States, January 2016. [ bib | full text on HAL ]
[201] Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average. In Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, 17th International Conference on Formal Engineering Methods, volume 9407 of Lecture Notes in Computer Science, pages 17--32, Paris, France, November 2015. Springer. [ bib | full text on HAL | .pdf ]
[200] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. A Work-Efficient Algorithm for Parallel Unordered Depth-First Search. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, Texas, United States, November 2015. [ bib | DOI | full text on HAL | http ]
[199] Arthur Charguéraud and François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In 6th International Conference on Interactive Theorem Proving (ITP), Nanjing, China, August 2015. [ bib | DOI | full text on HAL | http ]
[198] Martin Clochard, Jean-Christophe Filliâtre, and Andrei Paskevich. How to avoid proving the absence of integer overflows. In Arie Gurfinkel and Sanjit A. Seshia, editors, 7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), volume 9593 of Lecture Notes in Computer Science, pages 94--109, San Francisco, California, USA, July 2015. Springer. [ bib | full text on HAL ]
Keywords: Why3
[197] Catherine Lelay. How to express convergence for analysis in Coq. In The 7th Coq Workshop, Sophia Antipolis, France, June 2015. [ bib | full text on HAL ]
Keywords: Coq proof assistant ; Analysis ; Limits ; Filters ; Type-Classes ; Canonical Structures
[196] Sylvie Boldo. Stupid is as stupid does: Taking the square root of the square of a floating-point number. In Sergiy Bogomolov and Matthieu Martel, editors, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification, volume 317 of Electronic Notes in Theoretical Computer Science, pages 50--55, Seattle, WA, USA, April 2015. [ bib | DOI | full text on HAL ]
[195] Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions with set-theoretic types. part 2: Local type inference and type reconstruction. In Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India, January 2015. ACM Press. [ bib | full text on HAL ]
[194] Martin Clochard and Léon Gondelman. Double WP: vers une preuve automatique d'un compilateur. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015. [ bib | full text on HAL ]
[193] Sylvie Boldo. Formal verification of tricky numerical computations. In 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Würzburg, Germany, September 2014. Invited talk. [ bib | full text on HAL | http ]
[192] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Theory and practice of chunked sequences. In AndreasS. Schulz and Dorothea Wagner, editors, European Symposium on Algorithms, volume Lecture Notes in Computer Science, pages 25--36, Wroclaw, Poland, September 2014. Springer. [ bib | DOI | full text on HAL ]
Keywords: Data structure ; Sequence ; Chunk ; Amortization
[191] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. In Armin Biere and Roderick Bloem, editors, 26th International Conference on Computer Aided Verification, volume 8859 of Lecture Notes in Computer Science, pages 1--16, Vienna, Austria, July 2014. Springer. [ bib | full text on HAL | .pdf ]
In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this article, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Keywords: Why3
[190] Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Formalizing semantics with an automatic program verifier. In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), volume 8471 of Lecture Notes in Computer Science, pages 37--51, Vienna, Austria, July 2014. Springer. [ bib | full text on HAL ]
Keywords: Why3
[189] Martin Clochard. Automatically verified implementation of data structures based on AVL trees. In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), volume 8471 of Lecture Notes in Computer Science, pages 167--180, Vienna, Austria, July 2014. Springer. [ bib | full text on HAL ]
Keywords: Why3
[188] David Delahaye, Claude Marché, and David Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Paris, France, June 2014. EasyChair. [ bib | full text on HAL ]
Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financé pour 4 ans par le programme Ingénierie Numérique & Sécurité (INS) de l'Agence Nationale de la Recherche (ANR) et a débuté en septembre 2012 (voir le site web du projet : http://bware.lri.fr). Le consortium du projet BWare associe les partenaires académiques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R&D Centre Europe (MERCE), ClearSy, et OCamlPro

[187] David Delahaye, Catherine Dubois, Claude Marché, and David Mentré. The BWare project: Building a proof platform for the automated verification of B proof obligations. In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume 8477 of Lecture Notes in Computer Science, pages 290--293, Toulouse, France, June 2014. Springer. [ bib | full text on HAL ]
We introduce BWare, an industrial research project that aims to provide a mechanized framework to support the automated veri cation of proof obligations coming from the development of industrial applications using the B method and requiring high integrity. The methodology adopted consists in building a generic verification platform relying on di erent theorem provers, such as rst order provers and SMT (Satisfiability Modulo Theories) solvers. Beyond the multi-tool aspect of our methodology, the originality of this project also resides in the requirement for the veri cation tools to produce proof objects, which are to be checked independently. In this paper, we present some preliminary results of BWare, as well as some current major lines of work

[186] Véronique Benzaken, Évelyne Contejean, and Stefania Dumbrava. A Coq formalization of the relational data model. In Z. Shao, editor, European Symposium on Programming, LNCS 8410, Lecture Notes in Computer Science, pages 189--208, Grenoble, April 2014. Springer. [ bib | full text on HAL ]
[185] Martin Clochard, Claude Marché, and Andrei Paskevich. Verified programs with binders. In Programming Languages meets Program Verification (PLPV). ACM Press, 2014. [ bib | full text on HAL ]
[184] Giuseppe Castagna, Hyeonseung Im, Sergeï Lenglet, Kim Nguyen, Luca Padovani, and Zhiwu Xu. Polymorphic functions with set-theoretic types. part 1: Syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ]
[183] M. Clochard, S. Chaudhuri, and A. Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ]
[182] M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised JavaScript specification. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ]
[181] Sylvain Conchon and Mohamed Iguernelala. Tuning the Alt-Ergo SMT solver for B proof obligations. In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume 8477 of Lecture Notes in Computer Science, pages 294--297, Toulouse, France, June 2014. Springer. [ bib | DOI | full text on HAL ]
[180] Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. In Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib | full text on HAL ]
[179] Jean-Christophe Filliâtre. Le petit guide du bouturage, ou comment réaliser des arbres mutables en OCaml. In Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. https://www.lri.fr/~filliatr/publis/bouturage.pdf. [ bib ]
[178] Catherine Lelay. Coq passe le bac. In JFLA - Journées francophones des langages applicatifs, Fréjus, France, January 2014. [ bib ]
[177] Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Invariants for finite instances and beyond. In FMCAD, pages 61--68, Portland, Oregon, États-Unis, October 2013. [ bib | DOI | full text on HAL ]
Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.

[176] Guillaume Baudart, Florent Jacquemard, Louis Mandel, and Marc Pouzet. A synchronous embedding of Antescofo, a domain-specific language for interactive mixed music. In Thirteen International Conference on Embedded Software (EMSOFT'13), Montreal, Canada, September 2013. [ bib | full text on HAL | .pdf ]
Antescofo is recently developed software for musical score following and mixed music: it automatically, and in real-time, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems.

The system provides a programming language used by composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians and it continues to evolve according to their needs. Yet its semantics has only recently been formally defined. This paper presents a synchronous semantics for the core language of Antescofo and an alternative implementation based on an embedding inside an existing synchronous language, namely ReactiveML. The semantics reduces to a few rules, is mathematically precise and leads to an interpretor of only a few hundred lines. The efficiency of this interpretor compares well with that of the actual implementation: on all musical pieces we have tested, response times have been less than the reaction time of the human ear. Moreover, this embedding permitted the prototyping of several new programming constructs, some of which are described in this paper.

[175] Guillaume Baudart, Louis Mandel, and Marc Pouzet. Programming mixed music in ReactiveML. In ACM SIGPLAN Workshop on Functional Art, Music, Modeling and Design (FARM'13), Boston, USA, September 2013. Workshop ICFP 2013. [ bib | full text on HAL | .pdf ]
Mixed music is about live musicians interacting with electronic parts which are controlled by a computer during the performance. It allows composers to use and combine traditional instruments with complex synthesized sounds and other electronic devices. There are several languages dedicated to the writing of mixed music scores. Among them, the Antescofo language coupled with an advanced score follower allows a composer to manage the reactive aspects of musical performances: how electronic parts interact with a musician. However these domain specific languages do not offer the expressiveness of functional programming.

We embed the Antescofo language in a reactive functional programming language, ReactiveML. This approach offers to the composer recursion, higher order, inductive types, as well as a simple way to program complex reactive behaviors thanks to the synchronous model of concurrency on which ReactiveML is built. This article presents how to program mixed music in ReactiveML through several examples.

[174] Louis Mandel, Cédric Pasteur, and Marc Pouzet. Time refinement in a functional synchronous language. In Proceedings of 15th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP'13), Madrid, Spain, September 2013. [ bib | full text on HAL | .pdf ]
Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent.

We propose an extension of the synchronous model of concurrency, called reactive domains, to simplify the programming of such systems. Reactive domains allow the creation of local time scales and enable refinement, that is, the replacement of an approximation of a system with a more detailed version without changing its behavior as observed by the rest of the program.

Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We present an operational semantics for the extended language and a type system that ensures the soundness of programs.

[173] Catherine Lelay. A New Formalization of Power Series in Coq. In 5th Coq Workshop, pages 1--2, Rennes, France, July 2013. http://coq.inria.fr/coq-workshop/2013#Lelay. [ bib | full text on HAL ]
[172] Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, Lake Placid, USA, June 2013. Springer. [ bib | full text on HAL | .pdf ]
[171] Jean-Christophe Filliâtre. One logic to use them all. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, pages 1--20, Lake Placid, USA, June 2013. Springer. [ bib | full text on HAL ]
Keywords: Why3
[170] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. Preserving user proofs across specification changes. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE), volume 8164 of Lecture Notes in Computer Science, pages 191--201, Atherton, USA, May 2013. Springer. [ bib | full text on HAL ]
Keywords: Why3
[169] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 --- where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 125--128. Springer, March 2013. [ bib | full text on HAL ]
Keywords: Why3
[168] Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 41--60. Springer, March 2013. [ bib | full text on HAL ]
[167] Claude Marché and Asma Tafat. Calcul de plus faible précondition, revisité en Why3. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ]
[166] Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ]
[165] Jean-Christophe Filliâtre and Rémy El Sibaïe. Combine : une bibliothèque OCaml pour la combinatoire. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. http://www.lri.fr/~filliatr/combine/. [ bib | full text on HAL | .pdf ]
[164] Louis Mandel and Cédric Pasteur. Réactivité des systèmes coopératifs : le cas de ReactiveML. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. http://rml.lri.fr/jfla13. [ bib | full text on HAL | .pdf ]
La concurrence coopérative est un modèle de programmation très répandu. On peut par exemple l'utiliser en OCaml à travers des bibliothèques comme Lwt, Async ou Equeue. Il a de nombreux avantages tels que l'absence de courses critiques et des implantations légères et efficaces. Néanmoins, un des inconvénients majeurs de ce modèle est qu'il dépend de la discipline du programmeur pour garantir que le système est réactif : un processus peut empêcher les autres de s'exécuter.

ReactiveML est un langage qui étend OCaml avec des constructions de concurrence coopérative. Il propose une analyse statique, l'analyse de réactivité, qui permet de détecter les expressions qui risquent de produire des comportements non coopératifs. Dans cet article, nous présentons cette analyse statique qui se définit à l'aide d'un système de types et effets. Ainsi, comme le typage de données aide les programmeurs à détecter des erreurs d'exécution au plus tôt, l'analyse de réactivité aide à détecter des erreurs de concurrence.

[163] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Scheduling parallel programs by work stealing with private deques. In Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming, PPoPP '13, pages 219--228. ACM Press, February 2013. [ bib | DOI | full text on HAL ]
[162] Véronique Benzaken, Giuseppe Castagna, Kim Nguyen, and Jérôme Siméon. Static and dynamic semantics of NoSQL languages. In R. Cousot, editor, Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Roma, Italy, January 2013. ACM Press. [ bib | full text on HAL ]
[161] Sylvie Boldo. How to compute the area of a triangle: a formal revisit. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[160] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[159] Jean-Christophe Filliâtre. Deductive Program Verification. In Nate Foster, Philippa Gardner, Alan Schmitt, Gareth Smith, Peter Thieman, and Tobias Wrigstad, editors, Programming Languages Mentoring Workshop (PLMW 2013), Rome, Italy, January 2013. [ bib | full text on HAL ]
[158] Daisuke Ishii, Guillaume Melquiond, and Shin Nakajima. Inductive verification of hybrid automata with strongest postcondition calculus. In Einar Broch Johnsen and Luigia Petre, editors, Proceedings of the 10th Conference on Integrated Formal Methods, volume 7940 of Lecture Notes in Computer Science, pages 139--153, Turku, Finland, 2013. [ bib | DOI | full text on HAL ]
[157] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Proceedings of the Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 289--304, Kyoto, Japan, December 2012. [ bib | DOI | full text on HAL ]
[156] François Bobot and Jean-Christophe Filliâtre. Separation predicates: a taste of separation logic in first-order logic. In 14th International Conference on Formal Ingineering Methods (ICFEM), volume 7635 of Lecture Notes in Computer Science, Kyoto, Japan, November 2012. Springer. [ bib | full text on HAL | .pdf ]
This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.

[155] Vijay Saraswat, David Cunningham, Liana Hadarean, Louis Mandel, Avraham Shinnar, and Olivier Tardieu. Constrained types - future directions. In 18th International Conference on Principles and Practice of Constraint Programming, Québec City, Canada, October 2012. Position Paper. [ bib | full text on HAL | .pdf ]
The use of constraints in types is quite natural. Yet, integrating constraint based types into the heart of a modern, statically typed, object-oriented programming language is quite tricky. Over the last five years we have designed and implemented the constrained types framework in the programming language X10. In this paper we review the conceptual design, the practical implementation issues, and the many new questions that are raised. We expect the pursuit of these questions to be a profitable area of future work.

[154] Mário Pereira, Jean-Christophe Filliâtre, and Simão Melo de Sousa. ARMY: a deductive verification platform for ARM programs using Why3. In INForum 2012, September 2012. [ bib | .pdf ]
Unstructured (low-level) programs tend to be challenging to prove correct, since the control flow is arbitrary complex and there are no obvious points in the code where to insert logical assertions. In this paper, we present a system to formally verify ARM programs, based on a flow sequentialization methodology and a formalized ARM semantics. This system, built upon the why3 verification platform, takes an annotated ARM program, turns it into a set of purely sequential flow programs, translates these programs' instructions into the corresponding formalized opcodes and finally calls the Why3 VCGen to generate the verification conditions that can then be discharged by provers. A prototype has been implemented and used to verify several programming examples.

Keywords: Why3
[153] David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine Paulin-Mohring. Towards Provably Robust Watermarking. In ITP 2012, volume 7406 of Lecture Notes in Computer Science, August 2012. [ bib | full text on HAL | .pdf ]
Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.

Keywords: watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving
[152] Jean-Christophe Filliâtre. Combining Interactive and Automated Theorem Proving using Why3 (invited tutorial). In Zvonimir Rakamarić, editor, Second International Workshop on Intermediate Verification Languages (BOOGIE 2012), Berkeley, California, USA, July 2012. [ bib ]
[151] Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Cubicle: A parallel SMT-based model checker for parameterized systems. In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, Berkeley, California, USA, July 2012. Springer. [ bib | full text on HAL ]
Cubicle is a new model checker for verifying safety properties of parameterized systems. It implements a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiments done on classic and challenging mutual exclusion algorithms and cache coherence protocols show that Cubicle is effective and competitive with state-of-the-art model checkers.

[150] Louis Mandel and Florence Plateau. Scheduling and buffer sizing of n-synchronous systems: Typing of ultimately periodic clocks in Lucy-n. In Eleventh International Conference on Mathematics of Program Construction (MPC'12), Madrid, Spain, June 2012. [ bib | .pdf ]
Lucy-n is a language for programming networks of processes communicating through bounded buffers. A dedicated type system, termed a clock calculus, automatically computes static schedules of the processes and the sizes of the buffers between them.

In this article, we present a new algorithm which solves the subtyping constraints generated by the clock calculus. The advantage of this algorithm is that it finds schedules for tightly coupled systems. Moreover, it does not overestimate the buffer sizes needed and it provides a way to favor either system throughput or buffer size minimization.

[149] David Mentré, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. Discharging proof obligations from Atelier B using multiple automated provers. In Steve Reeves and Elvinia Riccobene, editors, ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z, volume 7316 of Lecture Notes in Computer Science, pages 238--251, Pisa, Italy, June 2012. Springer. http://hal.inria.fr/hal-00681781/en/. [ bib | full text on HAL ]
We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B's set theory into polymorphic first-order logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.

[148] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, IJCAR 2012: Proceedings of the 6th International Joint Conference on Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 67--81, Manchester, UK, June 2012. Springer. [ bib | DOI | full text on HAL ]
This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the Alt-Ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.

[147] Jean-Christophe Filliâtre, Andrei Paskevich, and Aaron Stump. The 2nd verified software competition: Experience report. In Vladimir Klebanov and Sarah Grebing, editors, COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, UK, June 2012. EasyChair. [ bib | full text on HAL | .pdf ]
We report on the second verified software competition. It was organized by the three authors on a 48 hours period on November 8--10, 2011. This paper describes the competition, presents the five problems that were proposed to the participants, and gives an overview of the solutions sent by the 29 teams that entered the competition.

[146] Jean-Christophe Filliâtre. Combining Interactive and Automated Theorem Proving in Why3 (invited talk). In Keijo Heljanko and Hugo Herbelin, editors, Automation in Proof Assistants 2012, Tallinn, Estonia, April 2012. [ bib ]
[145] Catherine Lelay and Guillaume 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. [ bib | full text on HAL ]
[144] Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), volume 7152 of Lecture Notes in Computer Science, pages 2--17, Philadelphia, USA, January 2012. Springer. [ bib | full text on HAL | .pdf ]
[143] Jean-Christophe Filliâtre. Verifying two lines of C with Why3: an exercise in program verification. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), volume 7152 of Lecture Notes in Computer Science, pages 83--97, Philadelphia, USA, January 2012. Springer. [ bib | .pdf ]
This article details the formal verification of a 2-line C program that computes the number of solutions to the n-queens problem. The formal proof of (an abstraction of) the C code is performed using the Why3 tool to generate the verification conditions and several provers (Alt-Ergo, CVC3, Coq) to discharge them. The main purpose of this article is to illustrate the use of Why3 in verifying an algorithmically complex program.

Keywords: Why3
[142] Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, and Mattias Ulbrich. The COST IC0701 verification competition 2011. In Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, volume 7421 of Lecture Notes in Computer Science. Springer, 2012. [ bib | full text on HAL | .pdf ]
[141] Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Built-in treatment of an axiomatic floating-point theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, pages 12--21, Manchester, UK, 2012. LORIA. [ bib ]
[140] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. LORIA. [ bib ]
[139] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, 18th International Symposium on Formal Methods, volume 7436 of Lecture Notes in Computer Science, pages 147--154. Springer, 2012. [ bib | full text on HAL ]
[138] Denis Cousineau and Olivier Hermant. A semantic proof that reducibility candidates entail cut elimination. In Ashish Tiwari, editor, 23nd International Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 133--148, Nagoya, Japan, 2012. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL ]
[137] Johannes Kanig, Edmond Schonberg, and Claire Dross. Hi-Lite: the convergence of compiler technology and program verification. In Ben Brosgol, Jeff Boleng, and S. Tucker Taft, editors, Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, pages 27--34, Boston, USA, 2012. ACM Press. [ bib ]
[136] Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science, pages 314--329. Springer, December 2011. [ bib | full text on HAL ]
[135] Louis Mandel, Florence Plateau, and Marc Pouzet. Static scheduling of latency insensitive designs with Lucy-n. In Formal Methods in Computer Aided Design (FMCAD 2011), Austin, TX, USA, October 2011. [ bib | full text on HAL | .pdf ]
Lucy-n is a dataflow programming language similar to Lustre extended with a buffer operator. This language is based on the n-synchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucy-n is also applicable to model Latency Insensitive Designs (LID). In order to model relay stations, we have to introduce a delay operator. Thanks to this new operator, a LID can be described by a Lucy-n program. Then, the Lucy-n compiler automatically provides static schedules for computation nodes and buffer sizes needed in the shell wrappers.

[134] François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 87--102, Saarbrücken, Germany, October 2011. [ bib | .pdf ]
[133] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53--64, Wroclaw, Poland, August 2011. https://hal.inria.fr/hal-00790310. [ bib | full text on HAL ]
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Keywords: Why3
[132] Claire Dross, Jean-Christophe Filliâtre, and Yannick Moy. Correct Code Containing Containers. In 5th International Conference on Tests and Proofs (TAP'11), volume 6706 of Lecture Notes in Computer Science, pages 102--118, Zurich, June 2011. Springer. [ bib | full text on HAL | .pdf ]
For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. As standards like DO-178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and user-provided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.

[131] Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Functory: A distributed computing library for Objective Caml. In Trends in Functional Programming, volume 7193 of Lecture Notes in Computer Science, pages 65--81, Madrid, Spain, May 2011. [ bib | .pdf ]
We present Functory, a distributed computing library for Objective Caml. The main features of this library include (1) a polymorphic API, (2) several implementations to adapt to different deployment scenarios such as sequential, multi-core or network, and (3) a reliable fault-tolerance mechanism. This paper describes the motivation behind this work, as well as the design and implementation of the library. It also demonstrates the potential of the library using realistic experiments.

[130] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of Lecture Notes in Computer Science, pages 45--59, Saarbrücken, Germany, April 2011. Springer. [ bib | DOI | full text on HAL | .pdf | Abstract ]
[129] Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. Divide and recycle: types and compilation for a hybrid synchronous language. In ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES'11), Chicago, USA, April 2011. [ bib | .pdf ]
Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the SUNDIALS library.

[128] Véronique Benzaken, Jean-Daniel Fekete, Pierre-Luc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: data-intensive interactive workflows for visual analytics. In Serge Abiteboul, Christoph Koch, and Tan Kian Lee, editors, International Conference on Data Engineering (ICDE). IEEE Comp. Soc. Press, April 2011. [ bib | full text on HAL ]
[127] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In Manfred Schmidt-Schauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21--30, Novi Sad, Serbia, 2011. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL | http | Abstract ]
[126] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153--167. Springer, January 2011. [ bib | full text on HAL ]
[125] Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib ]
[124] Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Une bibliothèque de calcul distribué pour Objective Caml. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib | .pdf ]
[123] Louis Mandel and Florence Plateau. Typage des horloges périodiques en Lucy-n. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib | .pdf ]
Lucy-n est un langage permettant de programmer des réseaux de processus communiquant à travers des buffers de taille bornée. La taille des buffers et les rythmes d'exécution relatifs des processus sont calculés par une phase de typage appelée calcul d'horloge. Ce typage nécessite la résolution d'un ensemble de contraintes de sous-typage. L'an dernier, nous avons proposé un algorithme de résolution de ces contraintes utilisant des méthodes issues de l'interprétation abstraite. Cette année nous présentons un algorithme tirant profit de toute l'information contenue dans les types.

[122] Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243--252, Tübingen, Germany, 2011. [ bib | DOI | full text on HAL ]
[121] David Baelde, Romain Beauxis, and Samuel Mimram. Liquidsoap: A high-level programming language for multimedia streaming. In Ivana Cerná, Tibor Gyimóthy, Juraj Hromkovic, Keith G. Jeffery, Rastislav Královic, Marko Vukolic, and Stefan Wolf, editors, 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11), volume 6543 of Lecture Notes in Computer Science, Nový Smokovec, Slovakia, January 2011. Springer. [ bib ]
[120] Véronique Benzaken, Jean-Daniel Fekete, Pierre-Luc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: data-intensive interactive workflows for visual analytics. In Serge Abiteboul, Christoph Koch, and Tan Kian Lee, editors, International Conference on Data Engineering (ICDE). IEEE Comp. Soc. Press, April 2011. [ bib ]
[119] Albert Benveniste, Benoit Caillaud, and Marc Pouzet. The Fundamentals of Hybrid Systems Modelers. In 49th IEEE International Conference on Decision and Control (CDC), Atlanta, Georgia, USA, December 15-17 2010. [ bib ]
[118] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. In Andrei Voronkov, editor, LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, Yogyakarta, Indonesia, October 2010. (short paper). [ bib ]
[117] Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. A deductive verification platform for cryptographic software. In 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33, Pisa, Italy, September 2010. Electronic Communications of the EASST. [ bib | http ]
[116] Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Artificial Intelligence, pages 127--141, Edinburgh, Scotland, July 2010. Springer. [ bib | full text on HAL | .pdf ]
[115] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the First Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147--162, Edinburgh, Scotland, July 2010. Springer. [ bib | DOI | full text on HAL ]
[114] Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. In Proceedings of the Third International Workshop on Numerical Software Verification, Edinburgh, Scotland, July 2010. NSV-8. [ bib | full text on HAL ]
[113] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, pages 143--159, Paris, France, June 2010. http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083. [ bib | full text on HAL ]
[112] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n: a n-synchronous extension of Lustre. In Tenth International Conference on Mathematics of Program Construction (MPC 2010), Québec, Canada, June 2010. [ bib | .pdf ]
Synchronous functional languages such as Lustre or Lucid Synchrone define a restricted class of Kahn Process Networks which can be executed with no buffer. Every expression is associated to a clock indicating the instants when a value is present. A dedicated type system, the clock calculus, checks that the actual clock of a stream equals its expected clock and thus does not need to be buffered. The n-synchrony relaxes synchrony by allowing the communication through bounded buffers whose size is computed at compile-time. It is obtained by extending the clock calculus with a subtyping rule which defines buffering points.

This paper presents the first implementation of the n-synchronous model inside a Lustre-like language called Lucy-n. The language extends Lustre with an explicit buffer construct whose size is automatically computed during the clock calculus. This clock calculus is defined as an inference type system and is parametrized by the clock language and the algorithm used to solve subtyping constraints. We detail here one algorithm based on the abstraction of clocks, an idea originally introduced in [84]. The paper presents a simpler, yet more precise, clock abstraction for which the main algebraic properties have been proved in Coq. Finally, we illustrate the language on various examples including a video application.

[111] Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 14--23, Washington D.C., USA, April 2010. [ bib | full text on HAL | PDF ]
[110] Louis Mandel, Florence Plateau, and Marc Pouzet. Clock typing of n-synchronous programs. In Designing Correct Circuits (DCC 2010), Paphos, Cyprus, March 2010. [ bib ]
[109] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n : une extension n-synchrone de Lustre. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL. [ bib ]
[108] Alessandro Cimatti, Anders Franzen, Alberto Griggio, Krishnamani Kalyanasundaram, and Marco Roveri. Tighter integration of BDDs and SMT for predicate abstraction. In Design, Automation & Test in Europe, Dresden. Germany, March 2010. IEEE. [ bib | full text on HAL ]
[107] Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL. [ bib ]
[106] Sebastian Maneth and Kim Nguyen. Xpath whole query optimization. In 36th International Conference on Very Large Data Bases (VLDB'2010), volume 3, pages 882--893, 2010. [ bib ]
[105] Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In John P. Gallagher and Janis Voigtländer, editors, Partial Evaluation and Program Manipulation, pages 63--72, Madrid, Spain, January 2010. ACM Press. [ bib | DOI | Abstract ]
[104] Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, and Guillaume Von Tokarski. Observation temps-réel de programmes Caml. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ]
[103] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n : une extension n-synchrone de Lustre. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ]
Les langages synchrones flot de données permettent de programmer des réseaux de processus communicant sans buffers. Pour cela, chaque flot est associé à un type d'horloges, qui indique les instants de présence de valeurs sur le flot. La communication entre deux processus f et g peut être faite sans buffer si le type du flot de sortie de f est égal au type du flot d'entrée de g. Un système de type, le calcul d'horloge, infère des types tels que cette condition est vérifiée. Le modèle n-synchrone a pour but de relâcher ce modèle de programmation en autorisant les communications à travers des buffers de taille bornée. En pratique, cela consiste à introduire une règle de sous-typage dans le calcul d'horloge.

Nous avons présenté l'année dernière un article décrivant comment abstraire des horloges pour vérifier la relation de sous-typage. Cette année, nous présentons un langage de programmation n-synchrone : Lucy-n. Dans ce langage, l'inférence des types d'horloges est paramétrable par l'algorithme de résolution des contraintes de sous-typage. Nous montrons ici un algorithme basé sur les travaux de l'an dernier et comment programmer en Lucy-n à travers l'exemple d'une application de traitement multimédia.

[102] Louis Mandel. Cours de ReactiveML. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ]
[101] Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Specifying generic Java programs: two case studies. In Claus Brabrand and Pierre-Etienne Moreau, editors, Tenth Workshop on Language Descriptions, Tools and Applications. ACM Press, 2010. [ bib | full text on HAL ]
[100] Paolo Herms. Certification of a chain for deductive program verification. In Yves Bertot, editor, 2nd Coq Workshop, satellite of ITP'10, 2010. [ bib | full text on HAL ]
[99] Marc Pouzet and Pascal Raymond. Modular static scheduling of synchronous data-flow networks: An efficient symbolic representation. In ACM International Conference on Embedded Software (EMSOFT'09), Grenoble, France, October 2009. [ bib ]
[98] Marc Pouzet and Pascal Raymond. Modular static scheduling of synchronous data-flow networks: An efficient symbolic representation. In ACM International Conference on Embedded Software (EMSOFT'09), Grenoble, France, October 2009. [ bib ]
[97] Stéphane Lescuyer and Sylvain Conchon. Improving Coq propositional reasoning using a lazy CNF conversion scheme. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of Combining Systems, 7th International Symposium, Proceedings, volume 5749 of Lecture Notes in Computer Science, pages 287--303, Trento, Italy, September 2009. Springer. [ bib | DOI ]
[96] 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. [ bib | full text on HAL | .pdf ]
We present Who, a tool for verifying effectful higher-order functions. It features Effect polymorphism, higher-order logic and the possibility to reason about state in the logic, which enable highly modular specifications of generic code. Several small examples and a larger case study demonstrate its usefulness. The Who tool is intended to be used as an intermediate language for verification tools targeting ML-like programming languages.

[95] Louis Mandel, Florence Plateau, and Marc Pouzet. The ReactiveML toplevel (tool demonstration). In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009. [ bib ]
[94] Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 59--74, Grand Bend, Canada, July 2009. Springer. [ bib | DOI ]
[93] Sylvie Boldo. Floats & Ropes: a case study for formal numerical program verification. In 36th International Colloquium on Automata, Languages and Programming, volume 5556 of Lecture Notes in Computer Science - ARCoSS, pages 91--102, Rhodos, Greece, July 2009. Springer. [ bib ]
[92] Clément Hurlin, François Bobot, and Alexander J. Summers. Size does matter : Two certified abstractions to disprove entailment in intuitionistic and classical separation logic. In International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), July 2009. Coq proofs: http://www-sop.inria.fr/everest/Clement.Hurlin/disprove.tgz. [ bib | full text on HAL | .pdf ]
We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A does not entail B. We provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).

[91] Paul Caspi, Jean-Louis Colaço, Léonard Gérard, Marc Pouzet, and Pascal Raymond. Synchronous Objects with Scheduling Policies: Introducing safe shared memory in Lustre. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Dublin, June 2009. [ bib ]
[90] Paul Caspi, Jean-Louis Colaço, Léonard Gérard, Marc Pouzet, and Pascal Raymond. Synchronous Objects with Scheduling Policies: Introducing safe shared memory in Lustre. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Dublin, June 2009. [ bib ]
[89] Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Relaxing synchronous composition with clock abstraction. In Hardware Design using Functional languages (HFL 09), pages 35--52, York, UK, March 2009. [ bib ]
[88] Jean-Christophe Filliâtre. Invited tutorial: Why --- an intermediate language for deductive program verification. In Hassen Saïdi and Natarajan Shankar, editors, Automated Formal Methods (AFM09), Grenoble, France, 2009. [ bib ]
[87] Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane Lescuyer. Faire bonne figure avec Mlpost. In Vingtièmes Journées Francophones des Langages Applicatifs, Saint-Quentin sur Isère, January 2009. INRIA. [ bib | .pdf ]
Cet article présente Mlpost, une bibliothèque Ocaml de dessin scientifique. Elle s'appuie sur Metapost, qui permet notamment d'inclure des fragments LATEX dans les figures. Ocaml offre une alternative séduisante aux langages de macros LATEX, aux langages spécialisés ou même aux outils graphiques. En particulier, l'utilisateur de Mlpost bénéficie de toute l'expressivité d'Ocaml et de son typage statique. Enfin Mlpost propose un style déclaratif qui diffère de celui, souvent impératif, des outils existants.

[86] Louis Mandel and Florence Plateau. Abstraction d'horloges dans les systèmes synchrones flot de données. In Vingtièmes Journées Francophones des Langages Applicatifs, Saint-Quentin sur Isère, January 2009. INRIA. [ bib | .pdf ]
Les langages synchrones flot de données tels que Lustre manipulent des séquences infinies de données comme valeurs de base. Chaque flot est associé à une horloge qui définit les instants où sa valeur est présente. Cette horloge est une information de type et un système de types dédié, le calcul d'horloges, rejette statiquement les programmes qui ne peuvent pas être exécutés de manière synchrone. Dans les langages synchrones existants, cela revient à se demander si deux flots ont la même horloge et repose donc uniquement sur l'égalité d'horloges. Des travaux récents ont montré l'intérêt d'introduire une notion relâchée du synchronisme, où deux flots peuvent être composés dès qu'ils peuvent être synchronisés par l'introduction d'un buffer de taille bornée (comme c'est fait dans le modèle SDF d'Edward Lee). Techniquement, cela consiste à remplacer le typage par du sous-typage. Ce papier est une traduction et amélioration technique de [84] qui présente un moyen simple de mettre en oeuvre ce modèle relâché par l'utilisation d'horloges abstraites. Les valeurs abstraites représentent des ensembles d'horloges concrètes qui ne sont pas nécessairement périodiques. Cela permet de modéliser divers aspects des logiciels temps-réel embarqués, tels que la gigue bornée présente dans les systèmes vidéo, le temps d'exécution des processus temps réel et, plus généralement, la communication à travers des buffers de taille bornée. Nous présentons ici l'algèbre des horloges abstraites et leurs principales propriétés théoriques.

[85] William Edmonson and Guillaume Melquiond. IEEE interval standard working group - P1788: current status. In Javier D. Bruguera, Marius Cornea, Debjit DasSarma, and John Harrison, editors, Proceedings of the 19th IEEE Symposium on Computer Arithmetic, pages 231--234, Portland, OR, USA, 2009. [ bib | DOI ]
[84] Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Abstraction of Clocks in Synchronous Data-flow Systems. In The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS), volume 5356 of Lecture Notes in Computer Science, pages 237--254, Bangalore, India, December 2008. [ bib | PDF | .pdf ]
Synchronous data-flow languages such as Lustre manage infinite sequences or streams as basic values. Each stream is associated to a clock which defines the instants where the current value of the stream is present. This clock is a type information and a dedicated type system --- the so-called clock-calculus --- statically rejects programs which cannot be executed synchronously. In existing synchronous languages, it amounts at asking whether two streams have the same clocks and thus relies on clock equality only. Recent works have shown the interest of introducing some relaxed notion of synchrony, where two streams can be composed as soon as they can be synchronized through the introduction of a finite buffer (as done in the SDF model of Edward Lee). This technically consists in replacing typing by subtyping. The present paper introduces a simple way to achieve this relaxed model through the use of clock envelopes. These clock envelopes are sets of concrete clocks which are not necessarily periodic. This allows to model various features in real-time embedded software such as bounded jitter as found in video-systems, execution time of real-time processes and scheduling resources or the communication through buffers. We present the algebra of clock envelopes and its main theoretical properties.

[83] 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 Press. [ bib | PDF | .pdf ]
This functional pearl proposes an ML implementation of the Garsia--Wachs algorithm. This somewhat obscure algorithm builds a binary tree with minimum weighted path length from weighted leaf nodes given in symmetric order. Our solution exhibits the usual benefits of functional programming (use of immutable data structures, pattern-matching, polymorphism) and nicely compares to the purely imperative implementation from The Art of Computer Programming.

[82] Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In Otmame Aït-Mohamed, César Muñoz, and Sofiène Tahar, editors, 21th International Conference on Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science. Springer, August 2008. [ bib | Slides | .pdf ]
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.

[81] V. Benzaken, G.Castagna, D. Colazzo, and C. Miachon. Pattern by example: Type-driven visual programming of XML queries". In 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, Valencia, Spain, July 2008. ACM Press. [ bib ]
[80] Sylvie Boldo, Marc Daumas, and Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. In Marc Daumas and Javier Bruguera, editors, Proceedings of the 8th Conference on Real Numbers and Computers, pages 113--122, Santiago de Compostela, Spain, July 2008. [ bib | full text on HAL | PDF ]
[79] Romain Bardou. Ownership, pointer arithmetic and memory separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [ bib | .pdf ]
[78] Gwenael Delaval, Alain Girault, and Marc Pouzet. A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ]
[77] Dariusz Biernacki, Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Clock-directed Modular Code Generation of Synchronous Data-flow Languages. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ]
[76] Évelyne Contejean and Xavier Urbain. The A3PAT approach. In Workshop on Certified Termination WScT08, Leipzig, Germany, May 2008. [ bib ]
[75] Louis Mandel and Florence Plateau. Interactive programming of reactive systems. In Proceedings of Model-driven High-level Programming of Embedded Systems (SLA++P'08), Electronic Notes in Computer Science, pages 44--59, Budapest, Hungary, April 2008. Elsevier Science Publishers. [ bib | PDF | .pdf ]
[74] Évelyne Contejean. Coccinelle, a Coq library for rewriting. In Types, Torino, Italy, March 2008. [ bib ]
[73] Giuseppe Castagna and Kim Nguyen. Typed iterators for XML. In James Hook and Peter Thiemann, editors, ICFP, pages 15--26, Victoria, BC, Canada, September 2008. ACM. [ bib ]
[72] François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 1--5, 2008. [ bib | DOI | PDF | .pdf | Abstract ]
[71] Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane 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), volume 198(2) of Electronic Notes in Computer Science, pages 51--69. Elsevier Science Publishers, 2008. [ bib | DOI ]
We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantical values for class representatives instead of canonized terms. Using semantical values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantical values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

[70] Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer. SAT-MICRO : petit mais costaud ! In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, January 2008. INRIA. [ bib | .ps ]
Le problème SAT, qui consiste `a déterminer si une formule booléenne est satisfaisable, est un des problèmes NP-complets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SAT-solvers modernes ont connu des progrès spectaculaires ces dix dernières années dans leurs performances, essentiellement grâce à deux optimisations: le retour en arrière non-chronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une étude formelle du fonctionnement de ces techniques ainsi qu'une réalisation en Ocaml d'un SAT-solver, baptisé SAT-MICRO, intégrant ces optimisations. Le fonctionnement de SAT-MICRO est décrit par un ensemble de règles d'inférence et la taille de son code, 70 lignes au total, permet d'envisager sa certification complète.

[69] Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib | PDF | .pdf ]
[68] Jean-Christophe Filliâtre. Gagner en passant à la corde. In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, January 2008. INRIA. [ bib | PDF | .pdf ]
Cet article présente une réalisation en Ocaml de la structure de cordes introduite par Boehm, Atkinson et Plass. Nous montrons notamment comment cette structure de données s'écrit naturellement comme un foncteur, transformant une structure de séquence en une autre structure de même interface. Cette fonctorisation a de nombreuses applications au-delà de l'article original. Nous en donnons plusieurs, dont un éditeur de texte dont les performances sur de très gros fichiers sont bien meilleures que celles des éditeurs les plus populaires.

[67] Louis Mandel and Luc Maranget. Programming in JoCaml (tool demonstration). In 17th European Symposium on Programming (ESOP'08), pages 108--111, Budapest, Hungary, April 2008. [ bib | PDF | .pdf ]
[66] Jean-Christophe Filliâtre. Using SMT solvers for deductive verification of C and Java programs. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, Princeton, USA, 2008. [ bib ]
[65] Yannick Moy. Sufficient preconditions for modular assertion checking. In Francesco Logozzo, Doron Peled, and Lenore Zuck, editors, 9th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 4905 of Lecture Notes in Computer Science, pages 188--202, San Francisco, California, USA, January 2008. Springer. [ bib | PDF | .pdf ]
[64] Stéphane Lescuyer and Sylvain Conchon. A reflexive formalization of a SAT solver in Coq. In Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, 2008. [ bib ]
[63] Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In Proceedings of the Ninth International Conference on Mathematics of Program Construction (MPC'08), pages 305--335, 2008. [ bib | DOI | .pdf ]
We present a Hoare logic for a call-by-value programming language equipped with recursive, higher-order functions, algebraic data types, and a polymorphic type system in the style of Hindley and Milner. It is the theoretical basis for a tool that extracts proof obligations out of programs annotated with logical assertions. These proof obligations, expressed in a typed, higher-order logic, are discharged using off-the-shelf automated or interactive theorem provers. Although the technical apparatus that we exploit is by now standard, its application to functional programming languages appears to be new, and (we claim) deserves attention. As a sample application, we check the partial correctness of a balanced binary search tree implementation.

[62] Dariusz Biernacki, Jean-Louis Colaço, and Marc Pouzet. Clock-directed Modular Code Generation from Synchronous Block Diagrams. In Workshop on Automatic Program Generation for Embedded Systems (APGES 2007), Salzburg, Austria, October 2007. [ bib | PDF | .pdf ]
[61] Sylvain Conchon and Jean-Christophe Filliâtre. A Persistent Union-Find Data Structure. In ACM SIGPLAN Workshop on ML, pages 37--45, Freiburg, Germany, October 2007. ACM Press. [ bib | PDF | .pdf ]
The problem of disjoint sets, also known as union-find, consists in maintaining a partition of a finite set within a data structure. This structure provides two operations: a function find returning the class of an element and a function union merging two classes. An optimal and imperative solution is known since 1975. However, the imperative nature of this data structure may be a drawback when it is used in a backtracking algorithm. This paper details the implementation of a persistent union-find data structure as efficient as its imperative counterpart. To achieve this result, our solution makes heavy use of imperative features and thus it is a significant example of a data structure whose side effects are safely hidden behind a persistent interface. To strengthen this last claim, we also detail a formalization using the Coq proof assistant which shows both the correctness of our solution and its observational persistence.

[60] Jean-Christophe Filliâtre. Formal Verification of MIX Programs. In Journées en l'honneur de Donald E. Knuth, Bordeaux, France, October 2007. http://knuth07.labri.fr/exposes.php. [ bib | PDF | .pdf ]
We introduce a methodology to formally verify MIX programs. It consists in annotating a MIX program with logical annotations and then to turn it into a set of purely sequential programs on which classical techniques can be applied. Contrary to other approaches of verification of unstructured programs, we do not impose the location of annotations but only the existence of at least one invariant on each cycle in the control flow graph. A prototype has been implemented and used to verify several programs from The Art of Computer Programming.

[59] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, 6th International Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 of Lecture Notes in Artificial Intelligence, pages 148--162, Liverpool,UK, September 2007. Springer. [ bib | DOI | Abstract ]
[58] Jean-François Couchot and Thierry Hubert. A Graph-based Strategy for the Selection of Hypotheses. In FTP 2007 - International Workshop on First-Order Theorem Proving, Liverpool, UK, September 2007. [ bib | PDF | .pdf ]
In previous works on verifying C programs by deductive approaches based on SMT provers, we proposed the heuristic of separation analysis to handle the most difficult problems. Nevertheless, this heuristic is not sufficient when applied on industrial C programs: it remains some Verification Conditions (VCs) that cannot be decided by any SMT prover, mainly due to their size. This work presents a strategy to select relevant hypotheses in each VC. The relevance of an hypothesis is the combination of two separated dependency analysis obtained by some graph traversals. The approach is applied on a benchmark issued from an industrial program verification.

[57] Jean-François Couchot and Stéphane Lescuyer. Handling polymorphism in automated deduction. In 21th International Conference on Automated Deduction (CADE-21), volume 4603 of LNCS (LNAI), pages 263--278, Bremen, Germany, July 2007. [ bib | PDF | .pdf ]
Polymorphism has become a common way of designing short and reusable programs by abstracting generic definitions from type-specific ones. Such a convenience is valuable in logic as well, because it unburdens the specifier from writing redundant declarations of logical symbols. However, top shelf automated theorem provers such as Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To this end, we present efficient reductions of polymorphism in both unsorted and many-sorted first order logics. For each encoding, we show that the formulas and their encoded counterparts are logically equivalent in the context of automated theorem proving. The efficiency keynote is to disturb the prover as little as possible, especially the internal decision procedures used for special sorts, e.g. integer linear arithmetic, to which we apply a special treatment. The corresponding implementations are presented in the framework of the Why/Caduceus toolkit.

[56] Jean-François Couchot and Frédéric Dadeau. Guiding the correction of parameterized specifications. In Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 176--194, Oxford, UK, July 2007. Springer. [ bib | PDF | .pdf ]
Finding inductive invariants is a key issue in many domains such as program verification, model based testing, etc. However, few approaches help the designer in the task of writing a correct and meaningful model, where correction is used for consistency of the formal specification w.r.t. its inner invariant properties. Meaningfulness is obtained by providing many explicit views of the model, like animation, counter-example extraction, and so on. We propose to ease the task of writing a correct and meaningful formal specification by combining a panel of provers, a set-theoretical constraint solver and some model-checkers.

[55] Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, 19th International Conference on Computer Aided Verification, volume 4590 of Lecture Notes in Computer Science, pages 173--177, Berlin, Germany, July 2007. Springer. [ bib | DOI | full text on HAL | PDF ]
[54] Yannick Moy. Union and cast in deductive verification. In Proceedings of the C/C++ Verification Workshop, volume Technical Report ICIS-R07015, pages 1--16. Radboud University Nijmegen, July 2007. [ bib | PDF | .pdf ]
[53] Malgorzata Biernacka and Dariusz Biernacki. Formalizing Constructions of Abstract Machines for Functional Languages in Coq. In 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), pages 84--99, Paris, France, June 2007. [ bib | PDF | .pdf ]
[52] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, pages 187--194, Montpellier, France, June 2007. [ bib | PDF | .pdf ]
This paper introduces a methodology to perform formal verification of floating-point C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floating-point arithmetic. The Caduceus first-order logic model for C programs is extended accordingly. Then verification conditions expressing the correctness of the programs are obtained in the usual way and can be discharged interactively with the Coq proof assistant, using an existing Coq formalization of floating-point arithmetic. This methodology is already implemented and has been successfully applied to several short floating-point programs, which are presented in this paper.

[51] Claude Marché and Hans Zantema. The termination competition. In Franz Baader, editor, 18th International Conference on Rewriting Techniques and Applications (RTA'07), volume 4533 of Lecture Notes in Computer Science, pages 303--313, Paris, France, June 2007. Springer. [ bib | Slides | PDF | .pdf ]
[50] Claude Marché, Hans Zantema, and Johannes Waldmann. The termination competition 2007. In Dieter Hofbauer and Alexander Serebrenik, editors, Extended Abstracts of the 9th International Workshop on Termination, WST'07, June 2007. http://www.lri.fr/~marche/termination-competition/. [ bib | http ]
[49] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Marco T. Morazán and Henrik Nilsson, editors, The Eighth Symposium on Trends in Functional Programming, volume TR-SHU-CS-2007-04-1, pages XII/1--13, New York, USA, April 2007. Seton Hall University. [ bib | .ps ]
This paper details the design and implementation of Ocamlgraph, a highly generic graph library for the programming language Ocaml. This library features a large set of graph data structures---directed or undirected, with or without labels on vertices and edges, as persistent or mutable data structures, etc.---and a large set of graph algorithms. Algorithms are written independently from graph data structures, which allows combining user data structure (resp. algorithm) with Ocamlgraph algorithm (resp. data structure). Genericity is obtained through massive use of the Ocaml module system and its functions, the so-called functors.

[48] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a generic graph library using ML functors. In Trends in Functional Programming (TFP'07), New York City, USA, April 2007. [ bib | PDF | .pdf ]
[47] Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV'07), pages 81--93, Braga, Portugal, March 2007. [ bib | PDF | .pdf ]
[46] Lionel Morel and Louis Mandel. Executable contracts for incremental prototypes of embedded systems. In Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA'07), pages 123--136. Elsevier Science Publishers, March 2007. [ bib | PDF | .pdf ]
[45] Yannick Moy and Claude Marché. Inferring local (non-)aliasing and strings for memory safety. In Heap Analysis and Verification (HAV'07), pages 35--51, Braga, Portugal, March 2007. [ bib | PDF | .pdf ]
[44] Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In John Rushby and N. Shankar, editors, Proceedings of the second workshop on Automated formal methods, pages 55--59. ACM Press, 2007. [ bib | DOI | PDF | .pdf ]
Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Ergo is capable of generating proof traces for CC(X). Alternatively, Ergo can also be called interactively as a simple oracle without further verification. It is currently used to prove correctness of C and Java programs as part of the Why platform.

[43] Sylvain Conchon, Évelyne Contejean, and Johannes Kanig. CC(X): Efficiently combining equality and solvable theories without canonizers. In Sava Krstic and Albert Oliveras, editors, SMT 2007: 5th International Workshop on Satisfiability Modulo, 2007. [ bib ]
[42] Sylvain Conchon and Jean-Christophe Filliâtre. Union-Find Persistant. In Dix-huitièmes Journées Francophones des Langages Applicatifs, pages 135--149. INRIA, January 2007. [ bib | PDF | .pdf ]
Le problème des classes disjointes, connu sous le nom de union-find, consiste à maintenir dans une structure de données une partition d'un ensemble fini. Cette structure fournit deux opérations : une fonction find déterminant la classe d'un élément et une fonction union réunissant deux classes. Une solution optimale et impérative, due à Tarjan, est connue depuis longtemps.

Cependant, le caractère impératif de cette structure de données devient gênant lorsqu'elle est utilisée dans un contexte où s'effectuent des retours en arrière (backtracking). Nous présentons dans cet article une version persistante de union-find dont la complexité est comparable à celle de la solution impérative. Pour obtenir cette efficacité, notre solution utilise massivement des traits impératifs. C'est pourquoi nous présentons également une preuve formelle de correction, pour s'assurer notamment du caractère persistant de cette solution.

[41] Sébastien Labbé, Jean-Pierre Gallois, and Marc Pouzet. Slicing communicating automata specifications for efficient model reduction. In 18th Australian Conference on Software Engineering (ASWEC), 2007. [ bib ]
[40] Claude Marché. Jessie: an intermediate language for Java and C verification. In Programming Languages meets Program Verification (PLPV), pages 1--2, Freiburg, Germany, 2007. ACM Press. [ bib | DOI ]
[39] Matthieu Sozeau. Subset coercions in Coq. In Thorsten Altenkirch and Conor Mc Bride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 237--252. Springer, 2007. [ bib | Slides | .pdf ]
We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the “Predicate subtyping” feature of PVS and following mathematical convention. The typing judgements can be translated to the Calculus of Inductive Constructions by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment.

[38] Matthieu Sozeau. Program-ing finger trees in Coq. In Ralf Hinze and Norman Ramsey, editors, 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, pages 13--24, Freiburg, Germany, 2007. ACM Press. [ bib | DOI | Slides | .pdf ]
Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent data structure with good performance. Their genericity permits developing a wealth of structures like ordered sequences or interval trees on top of a single implementation. However, the type systems used by current functional languages do not guarantee the coherent parameterization and specialization of Finger Trees, let alone the correctness of their implementation. We present a certified implementation of Finger Trees solving these problems using the Program extension of Coq. We not only implement the structure but also prove its invariants along the way, which permit building certified structures on top of Finger Trees in an elegant way.

[37] Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Mixing Signals and Modes in Synchronous Data-flow Systems. In ACM International Conference on Embedded Software (EMSOFT'06), Seoul, South Korea, October 2006. [ bib ]
[36] Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ]
[35] Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ]
[34] Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006. IEEE Comp. Soc. Press. [ bib ]
[33] Sylvie Boldo. Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms. In Ulrich Furbach and Natarajan Shankar, editors, Third International Joint Conference on Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 52--66, Seattle, USA, August 2006. Springer. [ bib | PDF | .pdf ]
[32] Nicolas Halbwachs and Louis Mandel. Simulation and verification of asynchronous systems by means of a synchronous model. In Sixth International Conference on Application of Concurrency to System Design (ACSD'06), pages 3--14, Turku, Finland, June 2006. [ bib | PDF | .pdf ]
[31] Ludovic Samper, Florence Maraninchi, Laurent Mounier, and Louis Mandel. GLONEMO: Global and accurate formal models for the analysis of ad hoc sensor networks. In Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06), Nice, France, May 2006. ACM Press. [ bib | PDF | .pdf ]
[30] Sylvie Boldo and César Muñoz. Provably faithful evaluation of polynomials. In Proceedings of the 21st Annual ACM Symposium on Applied Computing, volume 2, pages 1328--1332, Dijon, France, April 2006. [ bib | full text on HAL ]
[29] June Andronick and Boutheina Chetali. An Environment for Securing Smart Cards Embedded C Code. In International Conference on Research in Smart Cards (Esmart'06), 2006. [ bib ]
[28] Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. In Tarmo Uustalu, editor, Mathematics of Program Construction, MPC 2006, volume 4014 of Lecture Notes in Computer Science, Kuressaare, Estonia, July 2006. Springer. [ bib | PDF | .pdf ]
[27] Jean-Christophe Filliâtre. Itérer avec persistance. In Dix-septièmes Journées Francophones des Langages Applicatifs. INRIA, January 2006. [ bib | .ps.gz ]
[26] Claude Marché and Hans Zantema. The termination competition 2006. In Alfons Geser and Harald Sondergaard, editors, Extended Abstracts of the 8th International Workshop on Termination, WST'06, August 2006. http://www.lri.fr/~marche/termination-competition/. [ bib | http ]
[25] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06) [24]. [ bib ]
[24] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06), Charleston, South Carolina, USA, January 2006. [ bib ]
[23] Sylvie Boldo, Marc Daumas, William Kahan, and Guillaume Melquiond. Proof and certification for an accurate discriminant. In 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib | http ]
[22] Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005. IEEE Comp. Soc. Press. [ bib | .ps ]
[21] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05) [20]. [ bib ]
[20] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ]
[19] Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ]
[18] Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179--194. Springer, August 2005. [ bib | .ps ]
[17] Nicolas Oury. Extensionality in the Calculus of Constructions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 278--293. Springer, August 2005. [ bib ]
[16] June Andronick, Boutheina Chetali, and Christine Paulin-Mohring. Formal verification of security properties of smart card embedded source code. In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, International Symposium of Formal Methods Europe (FM'05), volume 3582 of Lecture Notes in Computer Science, Newcastle,UK, July 2005. Springer. [ bib ]
[15] Évelyne Contejean and Pierre Corbineau. Reflecting proofs in first-order logic with equality. In Robert Nieuwenhuis, editor, 20th International Conference on Automated Deduction (CADE-20), volume 3632 of Lecture Notes in Artificial Intelligence, pages 7--22, Tallinn, Estonia, July 2005. Springer. [ bib | DOI | Abstract ]
[14] Louis Mandel and Marc Pouzet. ReactiveML, a Reactive Extension to ML. In ACM International Conference on Principles and Practice of Declarative Programming (PPDP), pages 82--93, Lisboa, July 2005. [ bib | PDF | .pdf ]
[13] Louis Mandel and Farid Benbadis. Simulation of mobile ad hoc network protocols in ReactiveML. In Proceedings of Synchronous Languages, Applications, and Programming (SLAP'05), Edinburgh, Scotland, April 2005. Elsevier Science Publishers. [ bib | PDF | .pdf ]
[12] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 79--94. INRIA, March 2005. [ bib | .ps.gz ]
[11] Pierre Corbineau. Skip lists et arbres binaires de recherche probabilistes. In Seizièmes Journées Francophones des Langages Applicatifs, pages 99--112. INRIA, March 2005. [ bib ]
[10] Louis Mandel and Marc Pouzet. ReactiveML, un langage pour la programmation réactive en ML. In Seizièmes Journées Francophones des Langages Applicatifs, pages 1--16. INRIA, March 2005. [ bib | .ps ]
[9] Julien Signoles. Une approche fonctionnelle du modèle vue-contrôleur. In Seizièmes Journées Francophones des Langages Applicatifs, pages 63--78. INRIA, March 2005. [ bib ]
[8] 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, 2005. [ bib ]
[7] Sylvie Boldo and Jean-Michel Muller. Some functions computable with a fused-mac. In Paolo Montuschi and Eric Schwarz, editors, Proceedings of the 17th Symposium on Computer Arithmetic, pages 52--58, Cape Cod, USA, 2005. [ bib | .pdf ]
[6] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, August 2004. ACM Press. [ bib ]
[5] Jean-Christophe Filliâtre and Pierre Letouzey. Functors for Proofs and Programs. In Proceedings of The European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 370--384, Barcelona, Spain, April 2004. [ bib | PDF | .pdf ]
[4] Bart Jacobs, Claude Marché, and Nicole Rauch. Formal verification of a commercial smart card applet with multiple tools. In Algebraic Methodology and Software Technology, volume 3116 of Lecture Notes in Computer Science, Stirling, UK, July 2004. Springer. [ bib ]
[3] Évelyne Contejean. A certified AC matching algorithm. In Vincent van Oostrom, editor, 15th International Conference on Rewriting Techniques and Applications, volume 3091 of Lecture Notes in Computer Science, pages 70--84, Aachen, Germany, June 2004. Springer. [ bib | DOI | Abstract ]
[2] Pierre Corbineau. First-order reasoning in the Calculus of Inductive Constructions. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES 2003 : Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 162--177, Torino, Italy, April 2004. Springer. [ bib | .ps | .ps ]
[1] Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, 6th International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15--29, Seattle, WA, USA, November 2004. Springer. [ bib | .ps.gz ]

  PhD theses

[31] Catherine Lelay. Repenser la bibliothèque réelle de Coq : vers une formalisation de l’analyse classique mieux adaptée. Thèse de doctorat, Université Paris-Sud, June 2015. [ bib | full text on HAL ]
[30] Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Thèse d'habilitation, Université Paris-Sud, October 2014. [ bib | full text on HAL ]
[29] Alain Mebsout. Invariants inference for model checking of parameterized systems. Thèse de doctorat, Université Paris-Sud, September 2014. [ bib | full text on HAL ]
[28] Évelyne Contejean. Facettes de la preuve, Jeux de reflets entre démonstration automatique et preuve assisté. Thèse d'habilitation, Université Paris-Sud, June 2014. https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf. [ bib | full text on HAL ]
[27] Claire Dross. Generic Decision Procedures for Axiomatic First-Order Theories. Thèse de doctorat, Université Paris-Sud, April 2014. [ bib | full text on HAL ]
[26] Asma Tafat. Preuves par raffinement de programmes avec pointeurs. Thèse de doctorat, Université Paris-Sud, September 2013. [ bib | full text on HAL ]
[25] Mohamed Iguernelala. Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures. Thèse de doctorat, Université Paris-Sud, June 2013. [ bib | full text on HAL ]
[24] Cédric Auger. Compilation Certifiée de SCADE/LUSTRE. Thèse de doctorat, Université Paris-Sud, February 2013. http://tel.archives-ouvertes.fr/tel-00818169/. [ bib | full text on HAL ]
[23] Paolo Herms. Certification of a Tool Chain for Deductive Program Verification. Thèse de doctorat, Université Paris-Sud, January 2013. http://tel.archives-ouvertes.fr/tel-00789543. [ bib | full text on HAL ]
[22] Sylvain Conchon. SMT Techniques and their Applications: from Alt-Ergo to Cubicle. Thèse d'habilitation, Université Paris-Sud, December 2012. In English, http://www.lri.fr/~conchon/publis/conchonHDR.pdf. [ bib | .html ]
[21] Thi Minh Tuyen Nguyen. Taking architecture and compiler into account in formal proofs of numerical programs. Thèse de doctorat, Université Paris-Sud, June 2012. [ bib | full text on HAL | .pdf ]
[20] François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université Paris-Sud, December 2011. [ bib | full text on HAL | .pdf ]
[19] Jean-Christophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université Paris-Sud, December 2011. [ bib | .pdf ]
[18] Romain Bardou. Verification of Pointer Programs Using Regions and Permissions. Thèse de doctorat, Université Paris-Sud, October 2011. http://proval.lri.fr/publications/bardou11phd.pdf. [ bib | full text on HAL | .pdf ]
[17] Stéphane Lescuyer. Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq. Thèse de doctorat, Université Paris-Sud, January 2011. [ bib | full text on HAL | .pdf ]
[16] Xavier Urbain. Preuve automatique : techniques, outils et certification. Thèse d'habilitation, Université Paris-Sud 11, November 2010. [ bib ]
[15] Florence Plateau. Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ]
[14] Johannes Kanig. Spécification et preuve de programmes d'ordre supérieur. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ]
[13] Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [ bib | .pdf ]
[12] Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. Thèse de doctorat, Université Paris-Sud, December 2008. [ bib ]
[11] Thierry Hubert. Analyse Statique et preuve de Programmes Industriels Critiques. Thèse de doctorat, Université Paris-Sud, June 2008. [ bib | .pdf ]
[10] 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. [ bib | .pdf ]
[9] Nicolas Oury. Égalités et filtrages avec types dépendants dans le Calcul des Constructions Inductives. Thèse de doctorat, Université Paris-Sud, September 2006. [ bib ]
[8] Julien Signoles. Extension de ML avec raffinement : syntaxe, sémantiques et système de types. Thèse de doctorat, Université Paris-Sud, July 2006. [ bib ]
[7] June Andronick. Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocessur. Plateforme Java Card et Système d'exploitation. Thèse de doctorat, Université Paris-Sud, March 2006. [ bib ]
[6] Louis Mandel. Conception, Sémantique et Implantation de ReactiveML : un langage à la ML pour la programmation réactive. PhD thesis, Université Paris 6, 2006. [ bib | PDF | .pdf ]
[5] Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, December 2005. [ bib | .pdf ]
[4] Pierre Corbineau. Démonstration Automatique en Théorie des Types. Thèse de doctorat, Université Paris-Sud, September 2005. [ bib ]
[3] Pierre Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat, Université Paris-Sud, July 2004. [ bib | .ps.gz ]
[2] Jacek Chrzaszcz. Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw University, Poland and Université de Paris-Sud, January 2004. [ bib ]
[1] Mihai Rotaru. Sur une théorie unificatrice des modèles de concurrence. PhD thesis, Cluj University, Romania and Université de Paris-Sud, January 2004. [ bib ]

  Misc.

[68] Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pottier. VOCAL -- A Verified OCaml Library. ML Family Workshop, September 2017. [ bib | full text on HAL ]
[67] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.6, 2016. http://coq.inria.fr. [ bib | http ]
[66] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.lri.fr/download/manual-0.86.1.pdf. [ bib | full text on HAL | .pdf ]
[65] Thierry Vieville, Sylvie Boldo, Florent Masseglia, and Pierre Bernhard. Structures : organisation, complexité, dynamique des mot-clés au sens inattendu, April 2015. Article de vulgarisation sur pixees.fr. [ bib | full text on HAL ]
[64] Jacques Charles Mbiada Ndjanda. FCLLVM: un compilateur intégré à l'environnement Frama-C. Master's thesis, Université Paris-Diderot, 2014. https://www.lri.fr/~jmbiadan/public/cea_intership_v1.pdf. [ bib ]
[63] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.lri.fr/download/manual-0.82.pdf. [ bib | full text on HAL | .pdf ]
[62] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.81. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.81 edition, March 2013. http://why3.lri.fr/download/manual-0.81.pdf. [ bib | full text on HAL | .pdf ]
Keywords: Why3
[61] Jean-Christophe Filliâtre. Deductive program verification with Why3. Lecture notes for the First DigiCosme Spring School, https://www.lri.fr/~marche/DigiCosmeSchool/filliatre.html, 2013. [ bib ]
Keywords: Why3
[60] Martin Clochard. Proving programs with binders, automatically. Master's thesis, Master Parisien de Recherche en Informatique, 2013. [ bib ]
[59] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Adding decision procedures to SMT solvers using axioms with triggers. Submitted, 2013. [ bib | full text on HAL | .pdf ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists.

[58] Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo. 2013. [ bib | full text on HAL | http ]
[57] Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings., volume 7998 of Lecture Notes in Computer Science. Springer, 2013. [ bib | DOI | http ]
[56] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.80. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.80 edition, October 2012. https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf. [ bib | .pdf ]
Keywords: Why3
[55] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.73 edition, July 2012. [ bib | .pdf ]
Keywords: Why3
[54] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.72 edition, May 2012. [ bib | .pdf ]
Keywords: Why3
[53] Nicolas Lupinski, Joel Falcou, and Christine Paulin-Mohring. Sémantiques d'un langage de squelettes. http://www.lri.fr/~paulin/Skel, 2012. [ bib ]
[52] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. The Why3 platform, version 0.71. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.71 edition, October 2011. https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf. [ bib ]
Keywords: Why3
[51] Nuno Gaspar. Mechanized semantics into concurrent program verification. http://www.lri.fr/~gaspar/rgcoq.html, September 2011. A documented Coq library, work in progress. [ bib ]
[50] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, February 2011. http://why3.lri.fr/. [ bib ]
Keywords: Why3
[49] Yannick Moy and Claude Marché. The Jessie plugin for Deduction Verification in Frama-C --- Tutorial and Reference Manual. INRIA & LRI, 2011. http://krakatoa.lri.fr/. [ bib | PDF | http ]
[48] Philippe Audebaud and Christine Paulin-Mohring, editors. Science of Computer Programming. Special issue on the Mathematics of Program Construction (MPC 2008), volume 76. Elsevier Science Publishers, 2011. [ bib | DOI | http ]
[47] François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language, 2011. Preliminary report. http://hal.inria.fr/inria-00591414/. [ bib ]
[46] Catherine Lelay. étude de la différentiabilité et de l'intégrabilité en Coq : Application à la formule de d'Alembert pour l'équation des ondes. Master's thesis, Université Paris 7, 2011. http://www.lri.fr/~lelay/Rapport.pdf. [ bib ]
[45] Bernhard Beckert and Claude Marché, editors. Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science. Springer, January 2011. [ bib ]
[44] Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, July 2010. http://interstices.info/decoupe. [ bib | http ]
[43] Sylvie Boldo. L'informatique. Universcience web television, April 2010. Quiz 5-12, http://www.universcience.tv/media/1340/l-informatique.html. [ bib | full text on HAL ]
[42] Sylvie Boldo. C'est la faute à l'ordinateur! Interstices -- Idée reçue, February 2010. http://interstices.info/idee-recue-informatique-18. [ bib | full text on HAL ]
[41] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.3, 2010. http://coq.inria.fr. [ bib | http ]
[40] Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ]
[39] Sylvie Boldo. Demandez le programme! Interstices, February 2009. http://interstices.info/demandez-le-programme. [ bib | http ]
[38] Mohamed Iguernelala. Extension modulo Associativité-Commutativité de l'algorithme de clôture par congruence CC(X). Master's thesis, Université Paris-Sud, 2009. [ bib ]
[37] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ]
[36] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[35] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseo publications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf. [ bib | .pdf ]
[34] Asma Tafat. Invariants et raffinements en présence de partage. Master's thesis, Université Paris 6, 2009. [ bib | .pdf ]
[33] Arthur Milchior. Algorithme de matching, modulo égalité, incrémental, typé et persistant. Rapport de stage L3, 2009. [ bib ]
[32] Claude Marché. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification, Viinistu, Estonia, January 2009. http://krakatoa.lri.fr/ws/. [ bib | PDF | http ]
[31] Paolo Herms. Partial type inference with higher-order types. Master's thesis, Università di Pisa, 2009. [ bib ]
[30] Sylvie Boldo and Thierry Viéville. L'informatique, ce n'est pas pour les filles. Interstices, September 2008. http://interstices.info/idee-recue-informatique-5. [ bib | http ]
[29] Philippe Audebaud and Christine Paulin-Mohring, editors. Mathematics of Program Construction, MPC 2008, volume 5133 of Lecture Notes in Computer Science, Marseille, France, July 2008. Springer. [ bib | http ]
[28] Sylvie Boldo. Pourquoi mon ordinateur calcule-t-il faux? Interstices, April 2008. Podcast, http://interstices.info/a-propos-calcul-ordinateurs. [ bib | http ]
[27] Maxime Beauquier. Application du filtrage modulo associativité et commutativité (AC) à la réécriture de sous-termes modulo AC dans Coq. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ]
[26] François Bobot. Satisfiabilité de formules closes modulo une théorie avec égalité et prédicats. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ]
[25] Steven Gay. Analyse d'échappement de portée en ReactiveML. Master's thesis, Master Parisien de Recherche en Informatique, 2008. [ bib ]
[24] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. http://alt-ergo.lri.fr/. [ bib ]
[23] Sylvain Conchon and Évelyne Contejean. The Alt-Ergo automatic theorem prover. http://alt-ergo.lri.fr/, 2008. APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000. [ bib | http ]
[22] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ]
[21] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.2, 2008. http://coq.inria.fr. [ bib | http ]
[20] Matthieu Sozeau. User defined equalities and relations, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2. [ bib ]
[19] Matthieu Sozeau. Program, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2, http://coq.inria.fr/. [ bib | http ]
[18] Matthieu Sozeau. Type Classes. INRIA, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2. [ bib ]
[17] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[16] Johannes Kanig. Certifying a congruence closure algorithm in Coq using traces. Diplomarbeit, Technische Universität Dresden, April 2007. [ bib ]
[15] Romain Bardou. Invariants de classe et systèmes d'ownership. Master's thesis, Master Parisien de Recherche en Informatique, 2007. [ bib | PDF | .pdf ]
[14] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. CiME3, 2007. http://cime.lri.fr. [ bib | www: ]
[13] Jean-Christophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification, 2007. http://why.lri.fr/queens/. [ bib | PDF | http ]
[12] Louis Mandel and Luc Maranget. The JoCaml system, 2007. Software and documentation available at http://jocaml.inria.fr/. [ bib | http ]
[11] Alexandre Bertails. Langages synchrones avec horloges périodiques. Master's thesis, Master Parisien de Recherche en Informatique, September 2006. [ bib | PDF | .pdf ]
[10] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.1, July 2006. http://coq.inria.fr. [ bib | http ]
[9] Marc Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Université Paris-Sud, LRI, April 2006. [ bib | http ]
[8] Stéphane Lescuyer. Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes. Master's thesis, Master Parisien de Recherche en Informatique, 2006. [ bib ]
[7] Nicolas Ayache. Coopération d'outils de preuve interactifs et automatiques. Master's thesis, Université Paris 7, 2005. [ bib ]
[6] Évelyne Contejean. Coccinelle, 2005. http://www.lri.fr/~contejea/Coccinelle/coccinelle.html. [ bib | www: ]
[5] Matthieu Sozeau. Coercion par prédicats en Coq. Master's thesis, Université Paris 7, 2005. In French. [ bib | .pdf ]
[4] Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors. Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18,2004, Selected Papers, volume 3839 of Lecture Notes in Computer Science. Springer, 2005. [ bib ]
[3] Thierry Hubert. Certification des preuves de terminaison en Coq. Rapport de DEA, Université Paris 7, September 2004. http://www.lri.fr/~marche/hubert04rr.ps. [ bib | .ps ]
[2] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.0, April 2004. http://coq.inria.fr. [ bib | http ]
[1] G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 8.0, April 2004. [ bib | http ]

  Reports

[41] Lucas Baudin. Deductive verification with the help of abstract interpretation. Technical report, Univ Paris-Sud, November 2017. [ bib | full text on HAL ]
[40] Ilham Dami and Claude Marché. The CoLiS language: syntax, semantics and associated tools. Technical Report 0491, Inria, October 2017. [ bib | full text on HAL ]
[39] Clément Fumex, Claude Marché, and Yannick Moy. Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria, April 2017. [ bib | full text on HAL ]
[38] Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a Unix path resolution algorithm. Research Report RR-8987, Inria, December 2016. [ bib | full text on HAL ]
[37] David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. Research Report RR-8854, Inria Saclay Ile-de-France, February 2016. [ bib | full text on HAL ]
[36] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. https://hal.archives-ouvertes.fr/hal-01256434v3. [ bib | full text on HAL ]
In the context of deductive verication, it is customary today to handle programs with pointers using either separation logic, dynamic frames, or explicit memory models. Yet we can observe that in numerous programs, a large amount of code ts within the scope of Hoare logic, provided we can statically control aliasing. When this is the case, the code correctness can be reduced to simpler verication conditions which do not require any explicit memory model. This makes verication conditions more amenable both to automated theorem proving and to manual inspection and debugging. In this paper, we devise a method of such static aliasing control for a programming language featuring nested data structures with mutable components. Our solution is based on a type system with singleton regions and eects, which we prove to be sound.

[35] Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib | full text on HAL ]
[34] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Fast parallel graph-search with splittable and catenable frontiers. Technical report, Inria, January 2015. [ bib | full text on HAL ]
[33] Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. Research Report 1560, LRI, June 2013. [ bib | full text on HAL | http | .pdf ]
[32] Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie De Quatrebarbes, and Stéphane Laurent. Médiation scientifique : une facette de nos métiers de la recherche. Interne, Inria, March 2013. [ bib | full text on HAL | http ]
Dans ce monde devenu numérique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du numérique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen maîtrise, au delà des usages, les principaux fondements de cette mutation numérique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque collègue Inria intéressé à participer à ce volet de nos missions. Devenue une facette de notre métier, comme le rappelle le Plan Stratégique Inria [1], ce que nous appelons médiation scientifique en sciences du numérique (alias, " mecsci ") se professionnalise et change d'échelle. Et c'est environ 1 % de nos ressources qui a vocation à y être consacré. Pour tout l'institut on parle donc de près de 40 équivalents temps-plein distribués à travers le travail quotidien ou ponctuel de plusieurs centaines de collègues chercheurs, ingénieurs, communicants, etc.. Une telle énergie mérite d'être bien employée : au service des meilleurs objectifs ; vers des cibles bien définies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident à faire bouger les choses ; et avec une méthodologie efficace qui optimise ce que nous investissons dans de telles activités ; tout en respectant et en encourageant les dynamiques locales et individuelles indépendantes qui restent les sources vives de la médiation scientifique. Voilà pourquoi il y a juste besoin d'offrir en partage à chacune et chacun les éléments fondateurs et méthodologiques de cette médiation scientifique. Offrir aussi quelques bonnes pratiques très concrètes. On parle donc ici d'une organisation distribuée d'actions collaboratives d'où émerge le service public de popularisation scientifique visé. C'est ce que ce document se propose de décrire ici.

Keywords: médiation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public.
[31] Claude Marché and Asma Tafat. Weakest precondition calculus, revisited using Why3. Research Report RR-8185, INRIA, December 2012. [ bib | full text on HAL | .pdf ]
[30] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. Research Report RR-7986, INRIA, June 2012. [ bib | full text on HAL | .pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism.

Keywords: Quantifiers, Triggers, SMT Solvers, Theories
[29] Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. Technical report, Tech. Univ. Munich, 2012. http://www21.in.tum.de/~blanchet/tff1spec.pdf. [ bib | .pdf ]
[28] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: Mathematics and program. Research Report 7826, INRIA, December 2011. [ bib | full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.

Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis
[27] Asma Tafat and Claude Marché. Binary heaps formally verified in Why3. Research Report 7780, INRIA, October 2011. http://hal.inria.fr/inria-00636083/en/. [ bib | full text on HAL ]
Keywords: Why3
[26] Krishnamani Kalyanasundaram and Claude Marché. Automated generation of loop invariants using predicate abstraction. Research Report 7714, INRIA, August 2011. http://hal.inria.fr/inria-00615623/en/. [ bib | full text on HAL ]
[25] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011. [ bib | .pdf | Abstract ]
[24] Thi Minh Tuyen Nguyen and Claude Marché. Proving floating-point numerical programs by analysis of their assembly code. Research Report 7655, INRIA, 2011. http://hal.inria.fr/inria-00602266/en/. [ bib | full text on HAL ]
[23] Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. Research Report 7793, INRIA, 2011. http://hal.inria.fr/hal-00639977/en/. [ bib | full text on HAL ]
[22] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI, Université Paris Sud, December 2010. [ bib | PDF | .pdf | Abstract ]
[21] Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform (version 2). Technical Report 7128, INRIA, 2010. http://hal.inria.fr/inria-00439232/en/. [ bib | full text on HAL ]
[20] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement approach for correct-by-construction object-oriented programs. Technical Report 7310, INRIA, 2010. [ bib | full text on HAL ]
[19] Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Research Report 7412, INRIA, 2010. http://hal.inria.fr/inria-00525384/en/. [ bib | full text on HAL ]
[18] Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. Technical Report 7128, INRIA, 2009. http://hal.inria.fr/inria-00439232. [ bib | full text on HAL ]
[17] Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Modular specification of Java programs. Technical Report 7097, INRIA, 2009. [ bib | full text on HAL ]
This work investigates the question of modular specification of generic Java classes and methods. The first part introduces a specification language for Java programs. In the second part the language is used to specify an array sorting algorithm by selection. The third and the fourth parts define a syntax proposal for the specification a generic Java programs, through two examples. The former is the specification of the generic method for sorting arrays which comes in the java.util.Arrays class of the Java API. The latter is the specification of the java.util.HashMap class and its use for memoization.

[16] Ali Ayad. On formal methods for certifying floating-point C programs. Research Report 6927, INRIA, 2009. [ bib | full text on HAL ]
[15] Guillaume Melquiond and Sylvain Pion. Directed rounding arithmetic operations. Technical Report 2899, ISO C++ Standardization Committee, 2009. [ bib ]
[14] Jean-François Couchot, Alain Giorgetti, and Nicolas Stouls. Graph-based Reduction of Program Verification Conditions. Research Report 6702, INRIA Saclay -- Île-de-France, October 2008. [ bib | full text on HAL ]
[13] Évelyne Contejean, Julien Forest, and Xavier Urbain. Deep-Embedded Unification. Research Report 1547, Cédric laboratory, CNAM Paris, France, 2008. [ bib ]
[12] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq - version 2. Description of a Coq contribution, Université Paris Sud, December 2007. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[11] Yannick Moy. Checking C pointer programs for memory safety. Research Report 6334, INRIA, October 2007. [ bib | PDF | .pdf ]
[10] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. Research Report 1185, CEDRIC, May 2007. [ bib ]
[9] Louis Mandel and Luc Maranget. Programming in JoCaml -- extended version. Technical Report 6261, INRIA, 2007. [ bib | PDF | .pdf ]
[8] Louis Mandel. Prototype of AADL simulation in SCADE. ASSERT deliverable 4.3.2-2, ASSERT Project, November 2006. [ bib ]
[7] Julien Signoles. Towards a ML extension with Refinement: a Semantic Issue. Technical Report 1440, LRI, University of Paris Sud, March 2006. [ bib | .pdf ]
[6] Louis Mandel. Report on modeling GALS in SCADE. ASSERT deliverable 4.3.2-1, ASSERT Project, February 2006. [ bib ]
[5] Jean-Christophe Filliâtre. Backtracking iterators. Research Report 1428, LRI, Université Paris Sud, January 2006. [ bib | .ps.gz ]
[4] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq. Description of a Coq contribution, Université Paris Sud, January 2006. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[3] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Research Report DSIC II/01/05, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, February 2005. [ bib ]
[2] Vikrant Chaudhary. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A case study. Technical report, IIT internship report, July 2004. [ bib ]
[1] Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ]

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports


This page was generated by bibtex2html.