Publications

[61] 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), November 2012. [ bib ]
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.

[60] Mário Pereira, Jean-Christophe Filliâtre, and Sim ao Melo de Sousa. ARMY: a deductive verification platform for ARM programs using Why3. In INForum 2012, September 2012. [ bib ]
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.

[59] Jean-Christophe Filliâtre. Course notes EJCP 2012, chapter Vérification déductive de programmes avec Why3. June 2012. [ bib | http ]
[58] David Mentré, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. Discharging proof obligations from Atelier B using multiple automated provers. In ABZ Conference, Pisa, Italy, June 2012. [ bib | .pdf ]
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.

[57] 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 ]
[56] 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, 2012. Accepted for publication. http://hal.inria.fr/hal-00649240/en/. [ bib ]
[55] 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. EasyChair, 2012. [ bib | .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.

[54] Jean-Christophe Filliâtre. Vérification déductive de programmes avec Why3, Janvier 2012. Cours aux vingt-troisièmes Journées Francophones des Langages Applicatifs. [ bib | http ]
[53] Jean-Christophe Filliâtre. Verifying two lines of C with Why3: an exercise in program verification. In Verified Software: Theories, Tools and Experiments (VSTTE), Philadelphia, USA, January 2012. [ 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.

[52] Jean-Christophe Filliâtre. Deductive software verification. International Journal on Software Tools for Technology Transfer (STTT), 13(5):397-403, August 2011. [ bib | DOI | http ]
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.

[51] 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, Wroclaw, Poland, August 2011. [ bib | .pdf ]
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.

[50] Claire Dross, Jean-Christophe Filliâtre, and Yannick Moy. Correct Code Containing Containers. In 5th International Conference on Tests & Proofs (TAP'11), Zurich, June 2011. [ bib ]
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.

[49] Jean-Christophe Filliâtre and K. 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 ]
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.

[48] Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Functory : Une bibliothèque de calcul distribué pour Objective Caml. In Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib | .pdf ]
Cet article présente Functory, une bibliothèque de calcul distribué pour Objective Caml. Les principales caractéristiques de cette bibliothèque sont (1) une interface polymorphe, (2) plusieurs réalisations correspondant à des contextes d'utilisation différents et (3) un mécanisme de tolérance aux pannes. Cet article détaille la conception et la réalisation de Functory et montre son potentiel sur de nombreux exemples.

[47] M. Barbosa, J.-C. Filliâtre, J. Sousa Pinto, and B. 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 ]
[46] 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 Proceedings of the first Interactive Theorem Proving Conference, LNCS, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOL and ACL2). [ bib | http ]
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest scheme and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time this kind of mathematical proof is machine-checked.

[45] 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 ]
Pour mettre au point un programme, tant du point de vue de sa correction que de ses performances, il est naturel de chercher à observer son exécution. On peut ainsi chercher à observer la gestion de la mémoire, le temps passé dans une certaine partie du code, ou encore certaines valeurs calculées par le programme. De nombreux outils permettent de telles observations (moniteur système, profiler ou debugger génériques ou spécifiques au langage, instrumentation explicite du code, etc.). Ces outils ne proposent cependant que des analyses << après coup >> ou des observations très limitées. Cet article présente Ocamlviz, une bibliothèque pour instrumenter du code Ocaml et des outils pour visualiser ensuite son exécution, en temps-réel et de manière distante.

[44] 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 | .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.

[43] 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. LNCS/LNAI, July 2009. [ bib | .pdf ]
Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.

[42] 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 | .html ]
[41] 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, 2009. INRIA. [ bib | .pdf ]
Cet article présente Mlpost, une bibliothèque Ocaml de dessin scientifique. Elle s'appuie sur , 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.

[40] 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. [ bib | .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.

[39] Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, 2008. Short version of [35]. [ bib | .pdf ]
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure.

[38] Jean-Christophe Filliâtre. Gagner en passant à la corde. In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, 2008. INRIA. [ bib | .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.

[37] Jean-Christophe Filliâtre. Formal Verification of MIX Programs. In Journées en l'honneur de Donald E. Knuth, Bordeaux, France, October 2007. [ bib | .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.

[36] 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. English version of [30]. [ bib | .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.

[35] Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. Research Report 1474, LRI, Université Paris Sud, September 2007. [ bib | .pdf ]
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure. Additionally, we give some examples of semi-persistent data structures (arrays, lists and hash tables).

[34] 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, Lecture Notes in Computer Science, Berlin, Germany, July 2007. Springer-Verlag. [ bib | .pdf ]
[33] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, Montpellier, France, June 2007. [ bib | .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.

[32] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In 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 . 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.

[31] Jean-Christophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification. Unpublished, January 2007. [ bib | .ps ]
This article details the formal verification of a 2-lines C program which computes the number of solutions to the n-queens problem. The formal proof is performed using the Caduceus tool to generate the verification conditions and several provers (Simplify, Ergo, Coq) to discharge them. The main purpose of this article is to show how a complex behavior of a C program can be established with . The key is here the possibility to introduce an abstract model and to relate it to the source code using ghost statements.

[30] Sylvain Conchon and Jean-Christophe Filliâtre. Union-Find Persistant. In Dix-huitièmes Journées Francophones des Langages Applicatifs, Aix-les-bains, France, 2007. INRIA. [ bib | .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.

[29] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Trends in Functional Programming, volume 8. Intellect, 2007. [ bib ]
[28] Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. Supersedes [10]. [ bib | .pdf ]
Hash-consing is a technique to share values that are structurally equal. Beyond the obvious advantage of saving memory blocks, hash-consing may also be used to speedup fundamental operations and data structures by several orders of magnitude when sharing is maximal. This paper introduces an Ocaml hash-consing library that encapsulates hash-consed terms in an abstract datatype, thus safely ensuring maximal sharing. This library is also parameterized by an equality that allows the user to identify terms according to an arbitrary equivalence relation.

[27] Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. Also LRI Research Report 1428. [ bib | .pdf ]
Iterating over the elements of an abstract collection is usually done in ML using a fold-like higher-order function provided by the data structure. This article discusses a different paradigm of iteration based on purely functional, immutable cursors. Contrary to fold-like iterators, the iteration can be cleanly interrupted at any step. Contrary to imperative cursors (such as those found in C++ and Java libraries) it is possible to backtrack the iterator to a previous step. Several ways to iterate over binary trees are examined and close links with Gérard Huet's Zipper are established. Incidentally, we show the well-known two-lists implementation of functional queues arising from a Zipper-based breadth-first traversal.

[26] Nicolas Ayache and Jean-Christophe Filliâtre. Combining the Coq Proof Assistant with First-Order Decision Procedures. Unpublished, March 2006. [ bib | .ps ]
We present an integration of first-order automatic theorem provers into the Coq proof assistant. This integration is based on a translation from the higher-order logic of Coq, the Calculus of Inductive Constructions, to a polymorphic first-order logic. This translation is defined and proved sound in this paper. It includes not only the translation of terms and predicates belonging to the first-order fragment, but also several techniques to go well beyond: abstractions of higher-order sub-terms, case-analysis, mutually recursive functions and inductive types. This process has been implemented in the Coq proof assistant to call the decision procedures Simplify, CVC Lite, haRVey and Zenon through Coq tactics. The first experiments are promising.

[25] Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors. Types for Proofs and Programs International Workshop, TYPES 2004, volume 3839 of Lecture Notes in Computer Science. Springer-Verlag, 2006. [ bib ]
[24] Jean-Christophe Filliâtre. Itérer avec persistance. In Dix-septièmes Journées Francophones des Langages Applicatifs, Pauillac, France, 2006. INRIA. [ bib | .ps ]
L'énumération des éléments d'une structure de données est généralement réalisée en ML par l'intermédiaire d'une fonction d'ordre supérieur. Cet article présente une alternative, sous la forme d'itérateurs pas à pas, à l'instar de ce qui se fait en programmation orientée objets, mais basés sur des structures persistantes, de manière à permettre notamment un éventuel backtracking. Plusieurs façons de parcourir les arbres binaires sont examinées, et des liens étroits avec le Zipper de Gérard Huet sont établis.

[23] J.-C. Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332-240, 2006. [ bib | DOI | .ps ]
In 1971, C. A. R. Hoare gave the proof of correctness and termination of a rather complex algorithm, in a paper entitled Proof of a program: Find. It is a hand-made proof, where the program is given together with its formal specification and where each step is fully justified by a mathematical reasoning. We present here a formal proof of the same program in the system Coq, using the recent tactic of the system developed to establishing the total correctness of imperative programs. We follow Hoare's paper as close as possible, keeping the same program and the same specification. We show that we get exactly the same proof obligations, which are proved in a straightforward way, following the original paper. We also explain how more informal reasonings of Hoare's proof are formalized in the system Coq. This demonstrates the adequacy of the system Coq in the process of certifying imperative programs.

[22] Jean-Christophe Filliâtre. Program Verification using Coq. Introduction to the WHY tool, August 2005. Lecture Notes, TYPES Summer School 2005 (Göteborg, Sweden). [ bib | .ps.gz ]
[21] 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 ]
Cet article présente Ocamlgraph, une bibliothèque générique de graphes pour le langage de programmation Ocaml. L'originalité de cette bibliothèque est de proposer d'une part un grand nombre de structures de données différentes pour représenter les graphes - graphes orientés ou non, structures persistantes ou modifiées en place, sommets et arcs avec ou sans étiquettes, marques sur les sommets, etc. - et d'autre part des algorithmes sur les graphes écrits indépendamment de la structure de données représentant les graphes. Le codage de ces deux aspects originaux a été rendu possible par une utilisation massive du système de modules d'Ocaml et notamment de ses fonctions, les foncteurs.

[20] Jean-Christophe Filliâtre and Claude Marché. Multi-Prover Verification of C Programs. In Sixth International Conference on Formal Engineering Methods (ICFEM), volume 3308 of Lecture Notes in Computer Science, pages 15-29, Seattle, November 2004. Springer-Verlag. [ bib | .ps.gz ]
Our goal is the verification of C programs at the source code level using formal proof tools. Programs are specified using annotations such as pre- and postconditions and global invariants. An original approach is presented which allows to formally prove that a function implementation satisfies its specification and is free of null pointer dereferencing and out-of-bounds array access. The method is not bound to a particular back-end theorem prover. A significant part of the ANSI C language is supported, including pointer arithmetic and possible pointer aliasing. We describe a prototype tool and give some experimental results.

[19] J.-C. Filliâtre and P. 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 | .ps.gz ]
This paper presents the formal verification with the Coq proof assistant of several applicative data structures implementing finite sets. These implementations are parameterized by an ordered type for the elements, using functors from the ML module system. The verification follows closely this scheme, using the newly Coq module system. One of the verified implementation is the actual code for sets and maps from the Objective Caml standard library. The formalization refines the informal specifications of these libraries into formal ones. The process of verification exhibited two small errors in the balancing scheme, which have been fixed and then verified. Beyond these verification results, this article illustrates the use and benefits of modules and functors in a logical framework.

[18] Jean-Christophe Filliâtre. Introduction à la programmation fonctionnelle, 2004. Notes de cours de Master M1. [ bib | .ps.gz ]
[17] J.-C. Filliâtre and F. Pottier. Producing All Ideals of a Forest, Functionally. Journal of Functional Programming, 13(5):945-956, September 2003. [ bib | .ps.gz ]
We present a functional implementation of Koda and Ruskey's algorithm for generating all ideals of a forest poset as a Gray code. Using a continuation-based approach, we give an extremely concise formulation of the algorithm's core. Then, in a number of steps, we derive a first-order version whose efficiency is comparable to a C implementation given by Knuth.

[16] J.-C. Filliâtre. Verification of Non-Functional Programs using Interpretations in Type Theory. Journal of Functional Programming, 13(4):709-745, July 2003. English translation of [8]. [ bib | .ps.gz ]
We study the problem of certifying programs combining imperative and functional features within the general framework of type theory. Type theory constitutes a powerful specification language, which is naturally suited for the proof of purely functional programs. To deal with imperative programs, we propose a logical interpretation of an annotated program as a partial proof of its specification. The construction of the corresponding partial proof term is based on a static analysis of the effects of the program, and on the use of monads. The usual notion of monads is refined in order to account for the notion of effect. The missing subterms in the partial proof term are seen as proof obligations, whose actual proofs are left to the user. We show that the validity of those proof obligations implies the total correctness of the program. We also establish a result of partial completeness. This work has been implemented in the Coq proof assistant. It appears as a tactic taking an annotated program as argument and generating a set of proof obligations. Several nontrivial algorithms have been certified using this tactic.

[15] J.-C. Filliâtre. Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud, March 2003. [ bib | .ps.gz ]
[14] J.-C. Filliâtre. La supériorité de l'ordre supérieur. In Journées Francophones des Langages Applicatifs, pages 15-26, Anglet, France, Janvier 2002. [ bib | code | .ps.gz ]
Nous présentons ici une écriture fonctionnelle de l'algorithme de Koda-Ruskey, un algorithme pour engendrer une large famille de codes de Gray. En s'inspirant de techniques de programmation par continuation, nous aboutissons à un code de neuf lignes seulement, bien plus élégant que les implantations purement impératives proposées jusqu'ici, notamment par Knuth. Dans un second temps, nous montrons comment notre code peut être légèrement modifié pour aboutir à une version de complexité optimale. Notre implantation en Objective Caml rivalise d'efficacité avec les meilleurs codes C. Nous détaillons les calculs de complexité, un exercice intéressant en présence d'ordre supérieur et d'effets de bord combinés.

[13] J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. Deciding propositional combinations of equalities and inequalities. Unpublished, October 2001. [ bib | .ps ]
We address the problem of combining individual decision procedures into a single decision procedure. Our combination approach is based on using the canonizer obtained from Shostak's combination algorithm for equality. We illustrate our approach with a combination algorithm for equality, disequality, arithmetic inequality, and propositional logic. Unlike the Nelson-Oppen combination where the processing of equalities is distributed across different closed decision procedures, our combination involves the centralized processing of equalities in a single procedure. The termination argument for the combination is based on that for Shostak's algorithm. We also give soundness and completeness arguments.

[12] J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. ICS: Integrated Canonization and Solving (Tool presentation). In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV'2001, volume 2102 of Lecture Notes in Computer Science, pages 246-249. Springer-Verlag, 2001. [ bib ]
[11] J.-C. Filliâtre. Design of a proof assistant: Coq version 7. Research Report 1369, LRI, Université Paris Sud, October 2000. [ bib | .ps.gz ]
We present the design and implementation of the new version of the Coq proof assistant. The main novelty is the isolation of the critical part of the system, which consists in a type checker for the Calculus of Inductive Constructions. This kernel is now completely independent of the rest of the system and has been rewritten in a purely functional way. This leads to greater clarity and safety, without compromising efficiency. It also opens the way to the “bootstrap” of the Coq system, where the kernel will be certified using Coq itself.

[10] J.-C. Filliâtre. Hash consing in an ML framework. Research Report 1368, LRI, Université Paris Sud, September 2000. [ bib | .ps.gz ]
Hash consing is a technique to share values that are structurally equal. Beyond the obvious advantage of saving memory blocks, hash consing may also be used to gain speed in several operations (like equality test) and data structures (like sets or maps) when sharing is maximal. However, physical adresses cannot be used directly for this purpose when the garbage collector is likely to move blocks underneath. We present an easy solution in such a framework, with many practical benefits.

[9] J.-C. Filliâtre. A theory of monads parameterized by effects. Research Report 1367, LRI, Université Paris Sud, November 1999. [ bib | .ps.gz ]
Monads were introduced in computer science to express the semantics of programs with computational effects, while type and effect inference was introduced to mark out those effects. In this article, we propose a combination of the notions of effects and monads, where the monadic operators are parameterized by effects. We establish some relationships between those generalized monads and the classical ones. Then we use a generalized monad to translate imperative programs into purely functional ones. We establish the correctness of that translation. This work has been put into practice in the Coq proof assistant to establish the correctness of imperative programs.

[8] J.-C. Filliâtre. Preuve de programmes impératifs en théorie des types. Thèse de doctorat, Université Paris-Sud, July 1999. [ bib | .ps.gz ]
Nous étudions le problème de la certification de programmes mêlant traits impératifs et fonctionnels dans le cadre de la théorie des types.

La théorie des types constitue un puissant langage de spécification, naturellement adapté à la preuve de programmes purement fonctionnels. Pour y certifier également des programmes impératifs, nous commençons par exprimer leur sémantique de manière purement fonctionnelle. Cette traduction repose sur une analyse statique des effets de bord des programmes, et sur l'utilisation de la notion de monade, notion que nous raffinons en l'associant à la notion d'effet de manière générale. Nous montrons que cette traduction est sémantiquement correcte.

Puis, à partir d'un programme annoté, nous construisons une preuve de sa spécification, traduite de manière fonctionnelle. Cette preuve est bâtie sur la traduction fonctionnelle précédemment introduite. Elle est presque toujours incomplète, les parties manquantes étant autant d'obligations de preuve qui seront laissées à la charge de l'utilisateur. Nous montrons que la validité de ces obligations entraîne la correction totale du programme.

Nous avons implanté notre travail dans l'assistant de preuve Coq, avec lequel il est dès à présent distribué. Cette implantation se présente sous la forme d'une tactique prenant en argument un programme annoté et engendrant les obligations de preuve. Plusieurs algorithmes non triviaux ont été certifiés à l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de Knuth-Morris-Pratt).

[7] J.-C. Filliâtre and N. Magaud. Certification of sorting algorithms in the system Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999. [ bib | .ps.gz ]
We present the formal proofs of total correctness of three sorting algorithms in the system Coq, namely insertion sort, quicksort and heapsort. The implementations are imperative programs working in-place on a given array. Those developments demonstrate the usefulness of inductive types and higher-order logic in the process of software certification. They also show that the proof of rather complex algorithms may be done in a small amount of time - only a few days for each development - and without great difficulty.

[6] J.-C. Filliâtre. Proof of Imperative Programs in Type Theory. In International Workshop, TYPES '98, Kloster Irsee, Germany, volume 1657 of Lecture Notes in Computer Science. Springer-Verlag, March 1998. [ bib | .ps.gz ]
We present a new approach to certifying imperative programs, in the context of Type Theory. The key is a functional translation of imperative programs, which is made possible by an analysis of their effects. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic, but our approach also includes functional constructions. As a side-effect, we propose a way to eradicate the use of auxiliary variables in specifications. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.

[5] J.-C. Filliâtre. Finite Automata Theory in Coq: A constructive proof of Kleene's theorem. Research Report 97-04, LIP - ENS Lyon, February 1997. [ bib | .ps.Z ]
We describe here a development in the system Coq of a piece of Finite Automata Theory. The main result is the Kleene's theorem, expressing that regular expressions and finite automata define the same languages. From a constructive proof of this result, we automatically obtain a functional program that compiles any regular expression into a finite automata, which constitutes the main part of the implementation of grep-like programs. This functional program is obtained by the automatic method of extraction which removes the logical parts of the proof to keep only its informative contents. Starting with an idea of what we would have written in ML, we write the specification and do the proofs in such a way that we obtain the expected program, which is therefore efficient.

[4] J.-C. Filliâtre. A decision procedure for Direct Predicate Calculus: study and implementation in the Coq system. Research Report 96-25, LIP - ENS Lyon, February 1995. [ bib | .ps.Z ]
The paper of J. Ketonen and R. Weyhrauch A decidable fragment of Predicate Calculus defines a decidable fragment of first-order predicate logic - Direct Predicate Calculus - as the subset which is provable in Gentzen sequent calculus without the contraction rule, and gives an effective decision procedure for it. This report is a detailed study of this procedure. We extend the decidability to non-prenex formulas. We prove that the intuitionnistic fragment is still decidable, with a refinement of the same procedure. An intuitionnistic version has been implemented in the Coq system using a translation into natural deduction.

[3] J.-C. Filliâtre. Une procédure de décision pour le Calcul des Prédicats Direct : étude et implémentation dans le système Coq. Rapport de DEA, Ecole Normale Supérieure, Juillet 1994. [ bib | .dvi.gz ]
[2] J. Courant et J.-C. Filliâtre. Formalisation de la théorie des langages formels en Coq. Rapport de maîtrise, Ecole Normale Supérieure, Septembre 1993. [ bib | .dvi.gz ]
[1] J.-C. Filliâtre and C. Marché. ocamlweb, a literate programming tool for Objective Caml. Available at http://www.lri.fr/~filliatr/ocamlweb/. [ bib | http ]

This bibliography was built automatically using bibtex2html.
Homepage Français
Jean-Christophe.Filliatre[at]lri.fr (formatted with yamlpp).