@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.