@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,
NOTE = {To appear},
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 = 2001,
NOTE = {To appear},
URL = {http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz},
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 has been generated by bibtex2html 1.73