@article{boldo12jar, author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis}, title = {{Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program}}, journal = {Journal of Automated Reasoning}, year = {2012}, optvolume = {}, optnumber = {}, optpages = {}, optmonth = {}, note = {Accepted for publication. \url{http://hal.inria.fr/hal-00649240/en/}} }
@inproceedings{bobot12icfem, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre}, title = {Separation Predicates: a Taste of Separation Logic in First-Order Logic}, booktitle = {14th International Conference on Formal Ingineering Methods (ICFEM)}, month = {November}, year = 2012, type_publi = {icolcomlec}, topics = {team}, abstract = {This paper introduces \emph{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.} }
@inproceedings{filliatre12inforum, author = {M\'ario Pereira and Jean-Christophe Filli\^atre and Sim\~ao Melo de Sousa}, title = {{ARMY}: a Deductive Verification Platform for {ARM} Programs Using {Why3}}, month = {September}, year = 2012, type_publi = {icolcomlec}, topics = {team}, abstract = {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.}, booktitle = {INForum 2012} }
@inproceedings{filliatre12compare, author = {Jean-Christophe Filli\^atre and Andrei Paskevich and Aaron Stump}, title = {The 2nd Verified Software Competition: Experience Report}, booktitle = {COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems}, year = 2012, editor = {Vladimir Klebanov and Sarah Grebing}, publisher = {EasyChair}, type_publi = {icolcomlec}, topics = {team}, abstract = {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.}, url = {http://www.lri.fr/~filliatr/pub/compare2012.pdf} }
@inbook{filliatre12ejcp, author = {Jean-Christophe Filli\^atre}, title = {Course notes EJCP 2012}, chapter = {V\'erification d\'eductive de programmes avec {Why3}}, month = {June}, year = 2012, pdf = {http://why3.lri.fr/ejcp-2012/} }
@misc{filliatre12jfla, author = {Jean-Christophe Filli\^atre}, title = {Vérification déductive de programmes avec {Why3}}, month = {Janvier}, year = 2012, note = {Cours aux vingt-troisi\`emes Journ\'ees Francophones des Langages Applicatifs}, url = {http://why3.lri.fr/jfla-2012/} }
@inproceedings{filliatre12aipa, author = {Jean-Christophe Filli\^atre}, title = {{Combining Interactive and Automated Theorem Proving in Why3 (invited talk)}}, booktitle = {{Automation in Proof Assistants 2012}}, editor = {Keijo Heljanko and Hugo Herbelin}, month = {April}, year = 2012, address = {Tallinn, Estonia} }
@inproceedings{mentre12abz, author = {David Mentr\'e and Claude March\'e and Jean-Christophe Filli\^atre and Masashi Asuka}, title = {Discharging Proof Obligations from {Atelier~B} using Multiple Automated Provers}, booktitle = {ABZ Conference}, year = 2012, address = {Pisa, Italy}, month = {June}, abstract = {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.}, pdf = {http://www.lri.fr/~filliatr/publis/abz12.pdf} }
@inproceedings{filliatre12vstte, author = {Jean-Christophe Filli\^atre}, title = {Verifying Two Lines of {C} with {Why3}: an Exercise in Program Verification}, booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)}, month = {January}, year = 2012, address = {Philadelphia, USA}, url = {http://why3.lri.fr/queens/queens.pdf}, abstract = {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.} }
@article{filliatre11sttt, author = {Jean-Christophe Filli\^atre}, title = {Deductive Software Verification}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, month = aug, year = 2011, publisher = {Springer Berlin / Heidelberg}, volume = 13, number = 5, pages = {397-403}, issn = {1433-2779}, url = {http://dx.doi.org/10.1007/s10009-011-0211-0}, doi = {10.1007/s10009-011-0211-0}, abstract = {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.} }
@inproceedings{boogie11why3, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich}, title = {Why3: Shepherd Your Herd of Provers}, topics = {team}, booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages}, year = 2011, address = {Wroc\l{}aw, Poland}, month = {August}, url = {http://proval.lri.fr/submissions/boogie11.pdf}, abstract = {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.} }
@inproceedings{filliatre11tfp, author = {Jean-Christophe Filli\^atre and K. Kalyanasundaram}, title = {{Functory: A Distributed Computing Library for Objective Caml}}, booktitle = {Trends in Functional Programming}, year = 2011, series = {Lecture Notes in Computer Science}, volume = {7193}, pages = {65--81}, topics = {team}, address = {Madrid, Spain}, month = {May}, abstract = {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.} }
@inproceedings{dross11tap, author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy}, title = {{Correct Code Containing Containers}}, booktitle = {5th International Conference on Tests & Proofs (TAP'11)}, year = 2011, address = {Zurich}, month = {June}, topics = {team}, abstract = { 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.} }
@manual{baudin09acsl, title = {ACSL: ANSI/ISO C Specification Language, version 1.4}, author = {Patrick Baudin and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto}, year = 2009, note = {\url{http://frama-c.cea.fr/acsl.html}}, url = {http://frama-c.cea.fr/acsl.html} }
@inproceedings{filliatre11jfla, author = {Filli\^atre, Jean-Christophe and Kalyanasundaram, Krishnamani}, title = {Functory : Une biblioth\`eque de calcul distribu\'e pour {Objective Caml}}, year = 2011, booktitle = {Vingt-deuxi\`emes Journ\'ees Francophones des Langages Applicatifs}, month = jan, address = {La Bresse, France}, publisher = {INRIA}, url = {http://www.lri.fr/~filliatr/publis/jfla-2011.pdf}, abstract = {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.} }
@inproceedings{OpenCert2010, author = {M. Barbosa and J.-C. Filliâtre and J. Sousa Pinto and B. Vieira}, title = {{A Deductive Verification Platform for Cryptographic Software}}, booktitle = {{4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010)}}, year = 2010, address = {Pisa, Italy}, volume = {33}, publisher = {Electronic Communications of the EASST}, url = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461}, month = {September} }
@inproceedings{boldo10-itp, author = {Sylvie Boldo and François Clément and Jean-Christophe Filliâtre and Micaela Mayero and Guillaume Melquiond and Pierre Weis}, title = {{Formal Proof of a Wave Equation Resolution Scheme: the Method Error}}, booktitle = {Proceedings of the first Interactive Theorem Proving Conference}, year = 2010, series = {LNCS}, address = {Edinburgh, Scotland}, month = jul, publisher = {Springer}, note = {(merge of TPHOL and ACL2)}, topics = {team}, url = {http://hal.inria.fr/inria-00450789/en/}, abstract = {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. } }
@inproceedings{conchon10jfla, author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume}, title = {{Observation temps-réel de programmes Caml}}, topics = {team, lri}, type_publi = {colcomlec}, x-equipes = {demons PROVAL}, x-type = {article}, x-support = {actes_aux}, x-cle-support = {JFLA}, year = 2010, booktitle = {Vingt-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs}, month = jan, address = {Vieux-Port La Ciotat, France}, publisher = {INRIA}, abstract = { 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, \emph{profiler} ou \emph{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.}, url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf} }
@inproceedings{KanigFilliatre09wml, author = {Johannes Kanig and Jean-Christophe Filli\^atre}, title = {{Who: A Verifier for Effectful Higher-order Programs}}, booktitle = {ACM SIGPLAN Workshop on ML}, address = {Edinburgh, Scotland, UK}, topics = {team, lri}, type_publi = {icolcomlec}, type_digiteo = {conf_isbn}, month = aug, year = 2009, pdf = {http://www.lri.fr/~filliatr/ftp/publis/wml09.pdf}, abstract = {We present Who, a tool for verifying effectful higher-order functions. It features {\em 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.} }
@inproceedings{boldo09calculemus, author = {Sylvie Boldo and Jean-Christophe Filli\^atre and Guillaume Melquiond}, title = {Combining {C}oq and {G}appa for {C}ertifying {F}loating-{P}oint {P}rograms }, booktitle = {16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning}, year = {2009}, month = jul, publisher = {LNCS/LNAI}, topics = {team}, url = {http://www.lri.fr/~filliatr/publis/calculemus09.pdf}, abstract = { 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. } }
@inproceedings{mlpost09jfla, author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer}, title = {{Faire bonne figure avec Mlpost}}, booktitle = {{Vingtièmes Journ\'ees Francophones des Langages Applicatifs}}, year = 2009, address = {Saint-Quentin sur Isère}, publisher = {INRIA}, url = {http://www.lri.fr/~filliatr/ftp/publis/mlpost-fra.pdf}, abstract = {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.} }
@inproceedings{Filliatre08wml, author = {Jean-Christophe Filli\^atre}, title = {{A Functional Implementation of the Garsia--Wachs Algorithm}}, booktitle = {ACM SIGPLAN Workshop on ML}, publisher = {ACM}, year = 2008, address = {Victoria, British Columbia, Canada}, month = {September}, url = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf}, abstract = { 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 \emph{The Art of Computer Programming}.} }
@inproceedings{ConchonFilliatre08esop, author = {Sylvain Conchon and Jean-Christophe Filli\^atre}, title = {{Semi-Persistent Data Structures}}, booktitle = {17th European Symposium on Programming (ESOP'08)}, year = 2008, address = {Budapest, Hungary}, note = {Short version of~\cite{ConchonFilliatre07spdsrr}}, url = {http://www.lri.fr/~filliatr/ftp/publis/spds-esop08.pdf}, abstract = { A data structure is said to be \emph{persistent} when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called \emph{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.} }
@inproceedings{Filliatre07corde, author = {Jean-Christophe Filli\^atre}, title = {{Gagner en passant \`a la corde}}, booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs}, year = 2008, address = {\'Etretat, France}, publisher = {INRIA}, url = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf}, abstract = { Cet article pr\'esente une r\'ealisation en Ocaml de la structure de cordes introduite par Boehm, Atkinson et Plass. Nous montrons notamment comment cette structure de donn\'ees s'\'ecrit naturellement comme un foncteur, transformant une structure de s\'equence en une autre structure de même interface. Cette fonctorisation a de nombreuses applications au-del\`a de l'article original. Nous en donnons plusieurs, dont un \'editeur de texte dont les performances sur de tr\`es gros fichiers sont bien meilleures que celles des \'editeurs les plus populaires. } }
@inproceedings{Filliatre07mix, author = {Jean-Christophe Filli\^atre}, title = {{Formal Verification of MIX Programs}}, booktitle = {{Journées en l'honneur de Donald E. Knuth}}, year = 2007, address = {Bordeaux, France}, month = {October}, url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf}, abstract = {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 \emph{The Art of Computer Programming}.} }
@techreport{ConchonFilliatre07spdsrr, author = {Sylvain Conchon and Jean-Christophe Filli\^atre}, title = {{Semi-Persistent Data Structures}}, institution = {{LRI, Universit\'e Paris Sud}}, type = {{Research Report}}, number = {1474}, month = {September}, year = 2007, url = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf}, abstract = { 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).} }
@unpublished{Filliatre07queens, author = {Jean-Christophe Filli\^atre}, title = {{Queens on a Chessboard: an Exercise in Program Verification}}, note = {Unpublished}, month = {January}, year = 2007, url = {http://why.lri.fr/queens/queens.ps}, abstract = { 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 \caduceus. The key is here the possibility to introduce an abstract model and to relate it to the source code using ghost statements.} }
@inproceedings{filliatre07cav, author = {Jean-Christophe Filli\^atre and Claude March\'e}, title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program Verification}, editor = {Werner Damm and Holger Hermanns}, booktitle = {19th International Conference on Computer Aided Verification}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, address = {Berlin, Germany}, month = jul, year = {2007}, url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf} }
@inproceedings{BoldoFilliatre07, author = {Sylvie Boldo and Jean-Christophe Filli\^atre}, title = {{Formal Verification of Floating-Point Programs}}, booktitle = {18th IEEE International Symposium on Computer Arithmetic}, month = {June}, year = 2007, address = {Montpellier, France}, url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf}, abstract = { 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.} }
@inproceedings{ConchonFilliatre07wml, author = {Sylvain Conchon and Jean-Christophe Filli\^atre}, title = {{A Persistent Union-Find Data Structure}}, booktitle = {ACM SIGPLAN Workshop on ML}, publisher = {ACM}, pages = {37--45}, year = 2007, address = {Freiburg, Germany}, month = {October}, note = {English version of \cite{ConchonFilliatre06b}}, url = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf}, abstract = {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.} }
@inproceedings{ConchonFilliatre06b, author = {Sylvain Conchon and Jean-Christophe Filli\^atre}, title = {{Union-Find Persistant}}, booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs}, year = 2007, address = {Aix-les-bains, France}, publisher = {INRIA}, url = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf}, abstract = { Le problème des classes disjointes, connu sous le nom de \emph{union-find}, consiste à maintenir dans une structure de données une partition d'un ensemble fini. Cette structure fournit deux opérations : une fonction \emph{find} déterminant la classe d'un élément et une fonction \emph{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 (\emph{backtracking}). Nous présentons dans cet article une version persistante de \emph{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. } }
@inproceedings{ConchonFilliatre06, author = {Sylvain Conchon and Jean-Christophe Filli\^atre}, title = {{Type-Safe Modular Hash-Consing}}, booktitle = {ACM SIGPLAN Workshop on ML}, address = {Portland, Oregon}, note = {Supersedes~\cite{Filliatre00b}}, month = {September}, year = 2006, url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf}, abstract = { 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.} }
@incollection{conchon07tfpbook, author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles}, title = {{Designing a Generic Graph Library using ML Functors}}, booktitle = {Trends in Functional Programming}, publisher = {Intellect}, year = 2007, volume = 8, topics = {team, lri}, type_publi = {irevcomlec} }
@inproceedings{ocamlgraphTFP07, author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles}, title = {{Designing a Generic Graph Library using ML Functors}}, booktitle = {The Eighth Symposium on Trends in Functional Programming}, publisher = {Seton Hall University}, volume = {TR-SHU-CS-2007-04-1}, pages = {XII/1--13}, year = 2007, address = {New York, USA}, month = apr, topics = {team, lri}, type_publi = {icolcomlec}, abstract = { 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.}, url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp07.ps} }
@unpublished{AyacheFilliatre06, author = {Nicolas Ayache and Jean-Christophe Filli\^atre}, title = {{Combining the Coq Proof Assistant with First-Order Decision Procedures}}, note = {Unpublished}, month = {March}, year = 2006, url = {http://www.lri.fr/~filliatr/publis/coq-dp.ps}, abstract = { 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.} }
@inproceedings{Filliatre06, author = {Jean-Christophe Filli\^atre}, title = {{Backtracking iterators}}, booktitle = {ACM SIGPLAN Workshop on ML}, address = {Portland, Oregon}, note = {{Also LRI Research Report 1428}}, month = sep, year = {2006}, note = {English translation of \cite{Filliatre05}.}, url = {http://www.lri.fr/~filliatr/publis/enum2.pdf}, abstract = { 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\'erard 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.} }
@proceedings{Types2004, title = {{Types for Proofs and Programs International Workshop, TYPES 2004}}, year = 2006, editor = {Jean-Christophe Filli\^atre and Christine Paulin-Mohring and Benjamin Werner}, volume = 3839, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag} }
@inproceedings{Filliatre05, author = {Jean-Christophe Filli\^atre}, title = {{Itérer avec persistance}}, booktitle = {Dix-septi\`emes Journ\'ees Francophones des Langages Applicatifs}, year = 2006, address = {Pauillac, France}, publisher = {INRIA}, url = {http://www.lri.fr/~filliatr/publis/enum.ps}, abstract = { 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 \emph{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.} }
@misc{TypesSummerSchool2005, author = {Jean-Christophe Filli\^atre}, title = {{Program Verification using Coq. Introduction to the WHY tool}}, year = 2005, note = {Lecture Notes, TYPES Summer School 2005 (Göteborg, Sweden)}, month = aug, url = {http://www.lri.fr/~filliatr/publis/tss-2005.ps.gz} }
@misc{ipf, author = {Jean-Christophe Filli\^atre}, title = {{Introduction à la programmation fonctionnelle}}, year = 2004, note = {Notes de cours de Master M1}, url = {http://www.lri.fr/~filliatr/publis/ipf.ps.gz} }
@inproceedings{ConchonFilliatreSignoles05, author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles}, title = {Le foncteur sonne toujours deux fois}, booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs}, month = mar, year = 2005, publisher = {INRIA}, pages = {79--94}, url = {http://www.lri.fr/~filliatr/ftp/publis/jfla05.ps.gz}, abstract = { 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. } }
@inproceedings{FilliatreMarche04, author = {Jean-Christophe Filli\^atre and Claude March\'e}, title = {{Multi-Prover Verification of C Programs}}, booktitle = {Sixth International Conference on Formal Engineering Methods (ICFEM)}, year = 2004, address = {Seattle}, month = nov, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 3308, pages = {15--29}, url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz}, abstract = { 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.} }
@inproceedings{FilliatreLetouzey03, author = {J.-C. Filli\^atre and P. Letouzey}, title = {{Functors for Proofs and Programs}}, booktitle = {Proceedings of The European Symposium on Programming}, year = 2004, address = {Barcelona, Spain}, month = {April}, series = {Lecture Notes in Computer Science}, volume = 2986, pages = {370--384}, url = {http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz}, abstract = { 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. } }
@techreport{Filliatre03, author = {J.-C. Filli\^atre}, title = {{Why: a multi-language multi-prover verification tool}}, institution = {{LRI, Universit\'e Paris Sud}}, type = {{Research Report}}, number = {1366}, month = {March}, year = 2003, url = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz} }
@article{FilliatrePottier02, author = {J.-C. Filli{\^a}tre and F. Pottier}, title = {{Producing All Ideals of a Forest, Functionally}}, journal = {Journal of Functional Programming}, volume = 13, number = 5, pages = {945--956}, month = {September}, year = 2003, url = {http://www.lri.fr/~filliatr/ftp/publis/kr-fp.ps.gz}, abstract = { 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.} }
@unpublished{FORS01, author = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar}, title = {Deciding Propositional Combinations of Equalities and Inequalities}, note = {Unpublished}, month = oct, year = 2001, url = {http://www.lri.fr/~filliatr/ftp/publis/ics.ps}, abstract = { 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.} }
@inproceedings{ICS, author = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar}, title = {{ICS: Integrated Canonization and Solving (Tool presentation)}}, booktitle = {Proceedings of CAV'2001}, editor = {G. Berry and H. Comon and A. Finkel}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 2102, pages = {246--249}, year = 2001 }
@inproceedings{Filliatre01a, author = {J.-C. Filli\^atre}, title = {La supériorité de l'ordre supérieur}, booktitle = {Journées Francophones des Langages Applicatifs}, pages = {15--26}, month = {Janvier}, year = 2002, address = {Anglet, France}, url = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz}, code = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps}, abstract = { 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.} }
@techreport{Filliatre00c, author = {J.-C. Filli\^atre}, title = {{Design of a proof assistant: Coq version 7}}, institution = {{LRI, Universit\'e Paris Sud}}, type = {{Research Report}}, number = {1369}, month = {October}, year = 2000, url = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz}, abstract = { 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.} }
@techreport{Filliatre00b, author = {J.-C. Filli\^atre}, title = {{Hash consing in an ML framework}}, institution = {{LRI, Universit\'e Paris Sud}}, type = {{Research Report}}, number = {1368}, month = {September}, year = 2000, url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing.ps.gz}, abstract = { 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.} }
@misc{ocamlweb, author = {J.-C. Filli\^atre and C. March\'e}, title = {{ocamlweb, a literate programming tool for Objective Caml}}, note = {Available at \url{http://www.lri.fr/~filliatr/ocamlweb/}}, url = {http://www.lri.fr/~filliatr/ocamlweb/} }
@article{Filliatre00a, author = {J.-C. Filli\^atre}, title = {{Verification of Non-Functional Programs using Interpretations in Type Theory}}, journal = {Journal of Functional Programming}, volume = 13, number = 4, pages = {709--745}, month = {July}, year = 2003, note = {English translation of~\cite{Filliatre99}.}, url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, abstract = {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.} }
@article{Filliatre99c, author = {J.-C. Filli\^atre}, title = {{Formal Proof of a Program: Find}}, journal = {Science of Computer Programming}, year = 2006, volume = 64, pages = {332--240}, doi = {10.1016/j.scico.2006.10.002}, url = {http://www.lri.fr/~filliatr/ftp/publis/find.ps}, abstract = {In 1971, C.~A.~R.~Hoare gave the proof of correctness and termination of a rather complex algorithm, in a paper entitled \emph{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.} }
@techreport{Filliatre99b, author = {J.-C. Filli\^atre}, title = {{A theory of monads parameterized by effects}}, institution = {{LRI, Universit\'e Paris Sud}}, type = {{Research Report}}, number = {1367}, month = {November}, year = 1999, url = {http://www.lri.fr/~filliatr/ftp/publis/monads.ps.gz}, abstract = {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.} }
@phdthesis{Filliatre99, author = {J.-C. Filli\^atre}, title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}}, type = {Th{\`e}se de Doctorat}, school = {Universit\'e Paris-Sud}, year = 1999, month = {July}, url = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}, abstract = {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).} }
@inproceedings{FilliatreMagaud99, author = {J.-C. Filli\^atre and N. Magaud}, title = {{Certification of sorting algorithms in the system Coq}}, booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends}, year = 1999, abstract = {We present the formal proofs of total correctness of three sorting algorithms in the system Coq, namely \textit{insertion sort}, \textit{quicksort} and \textit{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.}, url = {http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz} }
@inproceedings{Filliatre98, author = {J.-C. Filli\^atre}, title = {{Proof of Imperative Programs in Type Theory}}, booktitle = {International Workshop, TYPES '98, Kloster Irsee, Germany}, publisher = {Springer-Verlag}, volume = 1657, series = {Lecture Notes in Computer Science}, month = mar, year = {1998}, abstract = {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.}, url = {http://www.lri.fr/~filliatr/ftp/publis/types98.ps.gz} }
@techreport{Filliatre97, author = {J.-C. Filli\^atre}, institution = {LIP - ENS Lyon}, number = {97--04}, title = {{Finite Automata Theory in Coq: A constructive proof of Kleene's theorem}}, type = {Research Report}, month = {February}, year = {1997}, abstract = {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 {\tt grep}-like programs. This functional program is obtained by the automatic method of {\em 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.}, url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR97/RR97-04.ps.Z} }
@techreport{Filliatre95, author = {J.-C. Filli\^atre}, institution = {LIP - ENS Lyon}, number = {96--25}, title = {{A decision procedure for Direct Predicate Calculus: study and implementation in the Coq system}}, type = {Research Report}, month = {February}, year = {1995}, abstract = {The paper of J. Ketonen and R. Weyhrauch \emph{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.}, url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-25.ps.Z} }
@techreport{Filliatre94, author = {J.-C. Filli\^atre}, month = {Juillet}, institution = {Ecole Normale Sup\'erieure}, title = {{Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct~: \'etude et impl\'ementation dans le syst\`eme Coq}}, type = {Rapport de {DEA}}, year = {1994}, url = {ftp://ftp.lri.fr/LRI/articles/filliatr/memoire.dvi.gz} }
@techreport{CourantFilliatre93, author = {J. Courant et J.-C. Filli\^atre}, month = {Septembre}, institution = {Ecole Normale Sup\'erieure}, title = {{Formalisation de la th\'eorie des langages formels en Coq}}, type = {Rapport de ma\^{\i}trise}, year = {1993}, url = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.dvi.gz}, url2 = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.ps.gz} }
This file was generated by bibtex2html 1.97pl3.