filliatre.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc filliatre.cite -ob filliatre.bib -c 'author : "Filli\^atre"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@mastersthesis{filliatre94,
author = {Jean-Christophe Filli{\^a}tre},
title = {Une proc{\'e}dure de d{\'e}cision pour le Calcul des
Pr{\'e}dicats Direct - Etude et impl{\'e}mentation dans le
syst{\`e}me Coq},
school = {LIP (ENS Lyon)},
year = 1994
}
@manual{CoqManual98,
title = {The {Coq Proof Assistant Reference Manual} Version 6.2},
author = {B. Barras and S. Boutin and C. Cornes and J. Courant and
D. Delahaye and D. de Rauglaudre and J.-C. Filli{\^a}tre and
E. Gim{\'e}nez and H. Herbelin and G. Huet and P. Loiseleur
and C. Mu{\~{n}}oz and
C. Murthy and C. Parent and C. Paulin-Mohring and
A. Sa{\"\i}bi and B. Werner},
organization = {{INRIA-Rocquencourt}-{CNRS}-{Universit{\'e} Paris Sud}-
{ENS Lyon}},
ftp = {ftp://ftp.inria.fr/INRIA/coq/V6.2/doc},
year = 1998,
month = may,
topics = {team, lri},
type_publi = {manuel},
clef_labo = {BBC+98M}
}
@unpublished{AyacheFilliatre06,
author = {Nicolas Ayache and Jean-Christophe Filli\^atre},
title = {Combining the {Coq} Proof Assistant with First-Order Decision Procedures},
month = mar,
year = 2006,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/coq-dp.pdf},
note = {\url{https://usr.lmf.cnrs.fr/~jcf/publis/coq-dp.pdf}},
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.}
}
@misc{Caduceus,
title = {The {Caduceus} tool for the verification of {C} programs},
author = {Jean-Christophe Filli\^atre and Thierry Hubert and Claude March\'e},
note = {\url{http://caduceus.lri.fr/}}
}
@manual{CoqManual99,
author = {B. Barras and S. Boutin and C. Cornes and J. Courant and
Y. Coscoy and D. Delahaye and D. de Rauglaudre and
J.C. Filli\^atre and E. Gim\'enez and H. Herbelin and
G. Huet and H. Laulh\`ere and P. Loiseleur and C. Mu{\~n}oz and
C. Murthy and C. Parent and C. Paulin and A. Sa{\"\i}bi and
B. Werner},
title = {{The Coq Proof Assistant Reference Manual -- Version V6.3}},
year = 1999,
month = jul,
type_publi = {manuel},
topics = {team},
note = {\url{http://coq.inria.fr/doc/main.html}},
abstract = {http://coq.inria.fr/doc/main.html}
}
@misc{Why,
author = {Jean-Christophe Filli\^atre},
title = {{The Why verification tool}},
year = 2002,
note = {\url{http://why.lri.fr/}},
url = {http://why.lri.fr/}
}
@misc{krakatoa,
author = {Jean-Christophe Filli{\^a}tre and Claude March\'e and Christine Paulin and Xavier Urbain},
title = {The \textsc{Krakatoa} proof tool},
year = 2003,
note = {\url{http://krakatoa.lri.fr/}}
}
@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},
year = 2004,
publisher = {Springer},
pages = {15--29},
url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz}
}
@article{boldo14camwa,
title = {{Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
year = {2014},
volume = {68},
number = {3},
pages = {325--352},
journal = {Computers and Mathematics with Applications},
hal = {http://hal.inria.fr/hal-00769201},
url = {http://www.sciencedirect.com/science/article/pii/S0898122114002636},
doi = {10.1016/j.camwa.2014.06.004},
topics = {team,lri},
type_publi = {irevcomlec}
}
@inproceedings{BoldoFilliatre07,
author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
doi = {10.1109/ARITH.2007.20},
title = {Formal Verification of Floating-Point Programs},
booktitle = {18th IEEE International Symposium on Computer Arithmetic},
pages = {187--194},
x-month = jun,
year = 2007,
x-address = {Montpellier, France},
topics = {team,lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus-floats.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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{conchon05jfla,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
title = {Le foncteur sonne toujours deux fois},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla05},
pages = {79--94},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jfla05.ps.gz}
}
@inproceedings{conchon07tfp,
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},
editor = {Marco T. Moraz\'an and Henrik Nilsson},
publisher = {Seton Hall University},
volume = {TR-SHU-CS-2007-04-1},
pages = {XII/1--13},
year = 2007,
address = {New York, USA},
month = apr,
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
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 = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp07.ps},
topics = {team, lri},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-editorial-board = {yes}
}
@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 Volume 8: Selected Papers of the $8^{th}$ International Symposium on Trends in Functional Programming (TFP'07), New York, USA},
editor = {Marco T. Moraz\'an},
publisher = {Intellect},
year = 2008,
volume = 8,
isbn = {9781841501963},
topics = {team, lri},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {ouvrage},
x-cle-support = {TFP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{conchon08tfp,
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 (TFP'07)},
month = {April},
year = 2007,
address = {New York City, USA},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {TFP},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{ConchonFilliatre06wml,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Type-Safe Modular Hash-Consing}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
month = sep,
year = 2006,
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing2.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing2.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre07jfla,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Union-Find Persistant}},
year = 2007,
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla07},
pages = {135--149},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
abstract = {
Le probl\`eme des classes disjointes, connu sous le nom de
\emph{union-find}, consiste \`a maintenir dans une structure de
donn\'ees une partition d'un ensemble fini. Cette structure fournit deux
op\'erations : une fonction \emph{find} d\'eterminant la classe d'un
\'el\'ement et une fonction \emph{union} r\'eunissant deux classes. Une
solution optimale et imp\'erative, due \`a Tarjan, est connue depuis
longtemps.
Cependant, le caract\`ere imp\'eratif de cette structure de donn\'ees
devient g\^enant lorsqu'elle est utilis\'ee dans un contexte o\`u
s'effectuent des retours en arri\`ere (\emph{backtracking}). Nous
pr\'esentons dans cet article une version persistante de
\emph{union-find} dont la complexit\'e est comparable \`a celle de la
solution imp\'erative. Pour obtenir cette efficacit\'e, notre solution
utilise massivement des traits imp\'eratifs. C'est pourquoi nous
pr\'esentons \'egalement une preuve formelle de correction, pour
s'assurer notamment du caract\`ere persistant de cette solution.
}
}
@techreport{ConchonFilliatre07rr,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {Semi-Persistent Data Structures}
}
@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 Press},
pages = {37--45},
year = 2007,
address = {Freiburg, Germany},
month = {October},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf-wml07.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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. },
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{Filliatre08wml,
author = {Jean-Christophe Filli\^atre},
title = {{A Functional Implementation of the Garsia--Wachs Algorithm}},
booktitle = {ACM SIGPLAN Workshop on ML},
publisher = {ACM Press},
year = 2008,
address = {Victoria, British Columbia, Canada},
month = {September},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/gw-wml08.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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}.},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre08esop,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
hal = {https://inria.hal.science/hal-04045849},
doi = {10.1007/978-3-540-78739-6_25},
title = {Semi-Persistent Data Structures},
crossref = {esop08},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-url = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@misc{why12app,
author = {J.-C. Filli\^atre and C. March\'e and Y. Moy and R. Bardou},
title = {Why version 2.30},
howpublished = {APP Deposit},
month = aug,
year = 2012,
note = {IDDN.FR.001.350004.000.S.P.2012.000.10000},
annote = {\url{http://why.lri.fr}}
}
@inproceedings{filliatr01icscav,
author = {Jean-Christophe Filli{\^a}tre and Sam Owre and Harald Rue{\ss} and Natarajan 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},
series = {Lecture Notes in Computer Science},
volume = 2102,
pages = {246--249},
year = 2001,
topics = {team, lri},
type_publi = {icolcomlec}
}
@misc{filliatr07queens,
author = {Jean-Christophe Filli\^atre},
title = {{Queens on a Chessboard:
an Exercise in Program Verification}},
topics = {team, lri},
type_publi = {autre},
type_digiteo = {no},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion},
year = 2007,
note = {\url{http://why.lri.fr/queens/}},
url = {http://why.lri.fr/queens/},
x-pdf = {http://why.lri.fr/queens/queens.ps}
}
@inproceedings{filliatre04icfem,
author = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
title = {Multi-Prover Verification of {C} Programs},
crossref = {icfem04},
year = {2004},
pages = {15--29},
topics = {team},
type_publi = {icolcomlec},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus.ps.gz}
}
@inproceedings{filliatre06jfla,
author = {Jean-Christophe Filli\^atre},
title = {It\'erer avec persistance},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla06},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/enum.ps.gz}
}
@inproceedings{filliatre07cav,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
Verification},
crossref = {cav07},
pages = {173--177},
topics = {team, lri},
hal = {https://hal.inria.fr/inria-00270820v1},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/cav07.pdf},
x-equipes = {demons PROVAL EXT},
x-type = {articlecourt},
x-support = {actes},
x-cle-support = {CAV},
doi = {10.1007/978-3-540-73368-3_21}
}
@techreport{Filliatre00rr1,
author = {Jean-Christophe Filli\^atre},
title = {{Design of a proof assistant: Coq version 7}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = 1369,
month = oct,
year = 2000,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/coqv7.ps.gz},
hal = {https://hal.inria.fr/hal-02890416},
topics = {team, lri},
type_publi = {interne}
}
@techreport{Filliatre00rr2,
author = {Jean-Christophe 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 = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing.ps.gz},
topics = {team, lri},
type_publi = {interne}
}
@inproceedings{Filliatre01a,
author = {Jean-Christophe Filli\^atre},
title = {La sup\'eriorit\'e de l'ordre sup\'erieur},
booktitle = {Journ\'ees Francophones des Langages Applicatifs},
pages = {15--26},
month = jan,
year = 2002,
address = {Anglet, France},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/sos.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/sos.pdf},
code = {https://usr.lmf.cnrs.fr/~jcf/ftp/ocaml/misc/koda-ruskey.ps},
topics = {team, lri},
type_publi = {colcomlec}
}
@techreport{Filliatre03,
author = {Jean-Christophe Filli\^atre},
title = {{Why: a multi-language multi-prover verification tool}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = {1366},
note = {\url{https://usr.lmf.cnrs.fr/~jcf/publis/why-tool.ps.gz}},
month = mar,
year = 2003,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/why-tool.ps.gz},
topics = {team, lri},
type_publi = {interne}
}
@article{Filliatre03jfp,
author = {Jean-Christophe Filli\^atre},
title = {Verification of Non-Functional Programs
using Interpretations in Type Theory},
volume = 13,
journal = {Journal of Functional Programming},
number = 4,
pages = {709--745},
month = jul,
year = 2003,
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/jphd.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jphd.pdf},
type_publi = {irevcomlec},
topics = {team}
}
@article{Filliatre03jfpa,
author = {Jean-Christophe 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 = jul,
year = 2003,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jphd.ps.gz}
}
@techreport{Filliatre06rr1,
author = {Jean-Christophe Filli\^atre},
title = {{Backtracking iterators}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = 1428,
month = jan,
year = 2006,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/enum-rr.ps.gz},
topics = {team, lri},
type_publi = {interne},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {rapport}
}
@inproceedings{Filliatre06wml,
author = {Jean-Christophe Filli\^atre},
title = {{Backtracking iterators}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
month = sep,
year = 2006,
topics = {team, lri},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/enum2.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/enum2.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{Filliatre07corde,
author = {Jean-Christophe Filli\^atre},
title = {{Gagner en passant \`a la corde}},
year = 2008,
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
x-editorial-board = {yes},
x-international-audience = {no},
x-proceedings = {yes},
crossref = {jfla08},
address = {\'Etretat, France},
publisher = {INRIA},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/cordes.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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\^eme 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{\'e}es en l'honneur de Donald E. Knuth}},
year = 2007,
address = {Bordeaux, France},
month = {October},
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/verifmix.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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}.},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux}
}
@inproceedings{Filliatre98,
author = {Jean-Christophe Filli\^atre},
title = {{Proof of Imperative Programs in Type Theory}},
booktitle = {Proceedings of the TYPES'98 workshop},
year = 1998,
publisher = {Springer},
volume = 1657,
series = {Lecture Notes in Computer Science},
topics = {team},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/types98.ps.gz},
clef_labo = {Fil98E},
type_publi = {icolcomlec}
}
@phdthesis{Filliatre99,
author = {Jean-Christophe Filli\^atre},
title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
school = {Universit\'e Paris-Sud},
year = 1999,
month = jul,
topics = {team},
type_publi = {these},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/these.ps.gz}
}
@article{Filliatre99c,
author = {Jean-Christophe 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},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/find.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/find.pdf},
topics = {team, lri},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-cle-support = {SCP}
}
@techreport{Filliatre99rr,
author = {Jean-Christophe 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 = {https://usr.lmf.cnrs.fr/~jcf/publis/monads.ps.gz},
topics = {team, lri},
type_publi = {interne}
}
@inproceedings{FilliatreLetouzey04esop,
author = {Jean-Christophe Filli\^atre and Pierre Letouzey},
title = {{Functors for Proofs and Programs}},
booktitle = {Proceedings of The European Symposium on Programming},
year = 2004,
address = {Barcelona, Spain},
month = apr,
series = {Lecture Notes in Computer Science},
volume = 2986,
pages = {370--384},
topics = {team},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/fpp.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/fpp.pdf}
}
@inproceedings{FilliatreMagaud99,
author = {Jean-Christophe Filli\^atre and Nicolas Magaud},
title = {{Certification of Sorting Algorithms in the System Coq}},
booktitle = {Theorem Proving in Higher Order Logics:
Emerging Trends},
year = 1999,
address = {Nice, France},
topics = {team},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/Filliatre-Magaud.ps.gz},
type_publi = {icolcomlec}
}
@article{FilliatrePottier02,
author = {Jean-Christophe Filli\^atre 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,
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/kr-fp.pdf},
topics = {team, lri},
type_publi = {irevcomlec}
}
@inproceedings{filliatre08smt,
author = {Jean-Christophe Filli\^atre},
title = {{Using SMT solvers for deductive verification of C and Java programs}},
booktitle = {{SMT 2008: 6th International Workshop on Satisfiability Modulo}},
editor = {Clark Barrett and Leonardo de Moura},
year = 2008,
topics = { team},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes_aux},
x-cle-support = {SMT},
address = {Princeton, USA}
}
@inproceedings{filliatre09afm,
author = {Jean-Christophe Filli\^atre},
title = {{Invited tutorial: Why --- an intermediate language for deductive program verification}},
booktitle = {{Automated Formal Methods (AFM09)}},
editor = {Hassen Sa\"{\i}di and Natarajan Shankar},
year = 2009,
topics = { team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {AFM},
address = {Grenoble, France}
}
@misc{Ocamlweb,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {{Ocamlweb, a literate programming tool for Objective Caml}},
note = {\url{https://github.com/backtracking/ocamlweb/}},
url = {https://github.com/backtracking/ocamlweb/}
}
@manual{baudin08acsl,
title = {ACSL: ANSI/ISO C Specification Language},
author = {Patrick Baudin and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = 2008,
note = {\url{http://frama-c.cea.fr/acsl.html}},
url = {http://frama-c.cea.fr/acsl.html},
x-pdf = {http://frama-c.cea.fr/download/acsl_1.4.pdf},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {contrat},
x-support = {rapport}
}
@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},
x-pdf = {http://frama-c.cea.fr/download/acsl_1.4.pdf},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {contrat},
x-support = {rapport}
}
@manual{baudin20acsl,
title = {ACSL: ANSI/ISO C Specification Language, version 1.16},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = 2020,
url = {https://frama-c.com/html/acsl.html},
topics = {team}
}
@inproceedings{mlpost09jfla,
author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
title = {{Faire bonne figure avec Mlpost}},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/mlpost-fra.pdf},
abstract = {Cet article pr\'esente Mlpost, une biblioth\`eque 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\'eduisante aux langages de macros \LaTeX, aux langages
sp\'ecialis\'es ou m\^eme aux outils graphiques. En particulier,
l'utilisateur de Mlpost b\'en\'eficie de toute l'expressivit\'e
d'Ocaml et de son typage statique. Enfin Mlpost propose un style
d\'eclaratif qui diff\`ere de celui, souvent imp\'eratif, des outils existants.},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla09}
}
@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},
pages = {59--74},
year = {2009},
month = jul,
volume = {5625},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
address = {Grand Bend, Canada},
doi = {10.1007/978-3-642-02614-0_10},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-support = {actes},
topics = {team}
}
@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,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/wml09.pdf},
hal = {http://hal.inria.fr/hal-00777585},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
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{conchon10jfla,
author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe
and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume},
title = {{Observation temps-r\'eel de programmes Caml}},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla10},
url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf}
}
@inproceedings{boldo10-itp,
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 = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
booktitle = {Interactive Theorem Proving},
year = 2010,
series = {Lecture Notes in Computer Science},
x-address = {Edinburgh, Scotland},
x-month = jul,
publisher = {Springer},
x-editor = {Matt Kaufmann and Lawrence C. Paulson},
volume = 6172,
pages = {147--162},
hal = {http://hal.inria.fr/inria-00450789/en},
doi = {10.1007/978-3-642-14052-5_12/},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-cle-support = {ITProving},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{filliatre11jfla,
author = {Filli\^atre, Jean-Christophe and Kalyanasundaram, Krishnamani},
title = {Une biblioth\`eque de calcul distribu\'e pour {Objective Caml}},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla11},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jfla-2011.pdf}
}
@inproceedings{filliatre10-opencert,
author = {Manuel Barbosa and Jean-Christophe Filli\^atre and Jorge Sousa Pinto and B\'arbara 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},
month = {September},
volume = {33},
publisher = {Electronic Communications of the EASST},
url = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {OSSC},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-pays = {PT}
}
@misc{bibtex2html10app,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {Bibtex2html},
howpublished = {APP Deposit},
year = 2010,
annote = {\url{https://github.com/backtracking/bibtex2html/}}
}
@inproceedings{dross11tap,
author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy},
title = {{Correct Code Containing Containers}},
booktitle = {5th International Conference on Tests and Proofs (TAP'11)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6706},
pages = {102--118},
year = 2011,
address = {Zurich},
month = jun,
url = {http://proval.lri.fr/publications/dross11tap.pdf},
hal = {http://hal.inria.fr/hal-00777683},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {TAP},
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.}
}
@inproceedings{filliatre11tfp,
author = {Jean-Christophe Filli\^atre and Krishnamani 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},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {TFP},
x-equipes = {demons PROVAL},
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.},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/tfp11.pdf}
}
@manual{bobot11why3,
title = {The Why3 platform},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.64},
month = feb,
year = 2011,
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@misc{why3,
title = {The {Why3} platform},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@manual{why3manual071,
title = {The Why3 platform, version 0.71},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.71},
month = oct,
year = 2011,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
note = {\url{https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf}}
}
@manual{why3manual072,
title = {The Why3 platform, version 0.72},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.72},
month = may,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}
@manual{why3manual073,
title = {The Why3 platform, version 0.73},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.73},
month = jul,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}
@manual{why3manual080,
title = {The Why3 platform, version 0.80},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.80},
month = oct,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf},
note = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}}
}
@manual{why3manual081,
title = {The Why3 platform, version 0.81},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.81},
month = mar,
year = 2013,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.81.pdf},
note = {\url{http://why3.org/download/manual-0.81.pdf}},
hal = {http://hal.inria.fr/hal-00822856/}
}
@manual{why3manual082,
title = {The Why3 platform, version 0.82},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.82},
month = dec,
year = 2013,
topics = {team},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.82.pdf},
note = {\url{http://why3.org/download/manual-0.82.pdf}}
}
@manual{why3manual0861,
title = {The Why3 platform, version 0.86.1},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.86.1},
month = may,
year = 2015,
topics = {team},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.86.1.pdf},
note = {\url{http://why3.org/download/manual-0.86.1.pdf}}
}
@inproceedings{boogie11why3-short,
crossref = {boogie11why3},
booktitle = {Boogie},
address = {},
topics = {}
}
@inproceedings{boogie11why3,
topics = {team},
hal = {http://hal.inria.fr/hal-00790310},
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},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
pages = {53--64},
note = {\url{https://hal.inria.fr/hal-00790310}},
x-international-audience = {yes},
x-proceedings = {yes},
x-cle-support = {BOOGIE},
x-type = {actes_aux},
x-support = {article},
x-equipes = {demons PROVAL},
keywords = {Why3},
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.}
}
@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},
x-type = {article},
x-support = {revue},
x-equipes = {demons PROVAL},
x-cle-support = {STTT},
doi = {10.1007/s10009-011-0211-0},
url = {http://proval.lri.fr/publications/filliatre11sttt.pdf},
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.},
topics = {team},
x-equipes = {demons PROVAL},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@inproceedings{filliatre12vstte,
author = {Jean-Christophe Filli\^atre},
title = {Verifying Two Lines of {C} with {Why3}: an Exercise in Program Verification},
crossref = {vstte12},
pages = {83--97},
x-equipes = {demons PROVAL},
topics = {team},
keywords = {Why3},
url = {http://proval.lri.fr/publications/filliatre12vstte.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.}
}
@phdthesis{filliatre11hdr,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification},
year = 2011,
month = dec,
type = {Th\`{e}se d'habilitation},
school = {Universit{\'e} Paris-Sud},
type_publi = {these},
url = {https://usr.lmf.cnrs.fr/~jcf/hdr/memoire.pdf},
x-equipes = {demons PROVAL},
x-type = {habilitation},
x-support = {rapport},
topics = {team, proval}
}
@techreport{BCFMMW11rr,
hal_id = {hal-00649240},
hal = {http://hal.inria.fr/hal-00649240/en/},
title = {Wave Equation Numerical Resolution: Mathematics and Program},
author = {Boldo, Sylvie and Cl\'ement, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
abstract = {We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.},
keywords = {Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis},
language = {Anglais},
affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI , ESTIME - INRIA Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rh{\^o}ne-Alpes / LIP Laboratoire de l'Informatique du Parall{\'e}lisme},
pages = {30},
type = {Research Report},
institution = {INRIA},
number = 7826,
year = 2011,
month = dec,
topics = {team},
x-equipes = {demons PROVAL ext},
x-support = {rapport}
}
@misc{vscomp2012,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich and Aaron Stump},
title = {The 2nd {V}erified {S}oftware {C}ompetition},
month = {November},
year = 2011,
note = {\url{https://sites.google.com/site/vstte2012/compet}}
}
@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'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z},
series = {Lecture Notes in Computer Science},
editor = {Steve Reeves and Elvinia Riccobene},
publisher = {Springer},
volume = {7316},
pages = {238--251},
year = 2012,
address = {Pisa, Italy},
month = jun,
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.},
obsoletepdf = {https://usr.lmf.cnrs.fr/~jcf/publis/abz12.pdf},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {ABZ},
x-pays = {jp},
hal_id = {hal-00681781},
hal = {http://hal.inria.fr/hal-00681781/en/},
note = {\url{http://hal.inria.fr/hal-00681781/en/}}
}
@inproceedings{bormer11foveoos,
author = {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli\^atre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March\'e and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and Bogdan Tofan and Julian Tschannen and Mattias Ulbrich},
title = {The {COST IC0701} Verification Competition 2011},
url = {http://proval.lri.fr/publications/bormer12foveoos.pdf},
crossref = {postfoveoos11},
x-type = {article},
x-equipes = {demons PROVAL ext},
topics = {team},
hal = {http://hal.inria.fr/hal-00789525}
}
@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,
topics = {team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {APA},
address = {Tallinn, Estonia}
}
@inproceedings{filliatre12boogie,
author = {Jean-Christophe Filli\^atre},
title = {{Combining Interactive and Automated Theorem Proving
using Why3 (invited tutorial)}},
booktitle = {{Second International Workshop on Intermediate Verification Languages (BOOGIE 2012)}},
editor = {Zvonimir Rakamari\'c},
month = {July},
year = 2012,
topics = {team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {BOOGIE},
address = {Berkeley, California, USA}
}
@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},
address = {Manchester, UK},
month = jun,
year = 2012,
hal = {http://hal.inria.fr/hal-00798777},
editor = {Vladimir Klebanov and Sarah Grebing},
publisher = {EasyChair},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {no},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {COMPARE},
x-type = {article},
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 = {https://usr.lmf.cnrs.fr/~jcf/pub/compare2012.pdf}
}
@inbook{filliatre12ejcp,
author = {Jean-Christophe Filli\^atre},
title = {Course notes EJCP 2012},
chapter = {V\'erification d\'eductive de programmes avec Why3},
topics = {team},
keywords = {Why3},
x-equipes = {demons PROVAL},
x-support = {diffusion},
x-type = {invitation},
month = jun,
year = 2012,
rawebnote = {\url{https://usr.lmf.cnrs.fr/~jcf/ejcp-2012/}},
pdf = {https://usr.lmf.cnrs.fr/~jcf/ejcp-2012/}
}
@inproceedings{filliatre12inforum,
author = {M\'ario Pereira and Jean-Christophe Filli\^atre and
Sim{\~a}o Melo de Sousa},
title = {{ARMY}: a Deductive Verification Platform for {ARM} Programs Using {Why3}},
month = {September},
year = 2012,
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {no},
x-equipes = {demons PROVAL ext},
x-support = {rapport},
x-cle-support = {INFORUM},
x-type = {article},
topics = {team},
keywords = {Why3},
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},
url = {http://inforum.org.pt/INForum2012/docs/20120013.pdf}
}
@inproceedings{bobot12icfem,
hal = {http://hal.inria.fr/hal-00825088},
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)},
volume = 7635,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Kyoto, Japan},
month = {November},
year = 2012,
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL},
x-support = {article},
x-cle-support = {ICFEM},
x-type = {actes},
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.},
url = {http://hal.inria.fr/hal-00825088}
}
@article{boldo13jar,
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 = {2013},
volume = {50},
number = {4},
pages = {423--456},
month = apr,
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL ext},
x-support = {revue},
x-type = {article},
x-cle-support = {JAR},
hal = {http://hal.inria.fr/hal-00649240/en/},
doi = {10.1007/s10817-012-9255-4},
topics = {team}
}
@article{CAOVerif,
author = {Jos\'e Bacelar Almeida and Manuel Barbosa and
Jean-Christophe Filli{\^a}tre and Jorge Sousa Pinto and B{\'a}rbara Vieira},
title = {{CAOVerif}: An Open-Source Deductive Verification Platform for Cryptographic Software Implementations},
journal = {Science of Computer Programming},
year = {2012},
optvolume = {},
optnumber = {},
optpages = {},
month = oct,
doi = {10.1016/j.scico.2012.09.019},
note = {Accepted for publication.},
topics = {team},
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL ext},
x-support = {revue},
x-cle-support = {SCP},
x-type = {article},
type_publi = {irevcomlec}
}
@inproceedings{filliatre13jfla,
author = {Jean-Christophe Filli\^atre and R\'emy El Siba\"{\i}e},
title = {{Combine} : une biblioth\`eque {OCaml} pour la combinatoire},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
note = {\url{https://github.com/backtracking/combine/}},
hal = {http://hal.inria.fr/hal-00779431},
url = {http://hal.inria.fr/hal-00779431}
}
@inproceedings{filliatre13esop-short,
crossref = {filliatre13esop},
booktitle = {ESOP},
series = {LNCS},
editor = {},
topics = {}
}
@inproceedings{filliatre13esop,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Why3 --- Where Programs Meet Provers},
booktitle = {Proceedings of the 22nd European Symposium on Programming},
month = mar,
year = 2013,
volume = {7792},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthias Felleisen and Philippa Gardner},
pages = {125--128},
hal = {http://hal.inria.fr/hal-00789533},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre13plmw,
author = {Jean-Christophe Filli\^atre},
title = {{Deductive Program Verification}},
booktitle = {{Programming Languages Mentoring Workshop (PLMW 2013)}},
editor = {Nate Foster and Philippa Gardner and Alan Schmitt and
Gareth Smith and Peter Thieman and Tobias Wrigstad},
month = {January},
hal = {http://hal.inria.fr/hal-00799190},
year = 2013,
topics = {team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {no},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
address = {Rome, Italy}
}
@inproceedings{filliatre13cade,
author = {Jean-Christophe Filli\^atre},
title = {One Logic To Use Them All},
crossref = {cade13},
pages = {1--20},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
hal = {http://hal.inria.fr/hal-00809651/en/}
}
@inproceedings{bobot13vstte,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
hal = {http://hal.inria.fr/hal-00875395},
title = {Preserving User Proofs Across Specification Changes},
crossref = {vstte13},
pages = {191--201},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@unpublished{filliatre13digicosme,
author = {Jean-Christophe Filli\^atre},
topics = {team},
keywords = {Why3},
title = {Deductive Program Verification with {Why3}},
year = 2013,
note = {Lecture notes for the First {DigiCosme} Spring School,
\url{https://usr.lmf.cnrs.fr/~jcf/digicosme-spring-school-2013/}}
}
@book{InfoPourTous2013Eyrolles,
hal = {http://hal.inria.fr/hal-00880268},
topics = {team},
author = {Benjamin Wack and Sylvain Conchon and Judica\"el Courant and Marc de Falco and Gilles Dowek and Jean-Christophe Filli\^atre and St\'ephane Gonnord},
title = {Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python},
publisher = {Eyrolles},
year = 2013,
month = aug,
pages = 408,
url = {http://www.eyrolles.com/Sciences/Livre/informatique-pour-tous-en-classes-preparatoires-aux-grandes-ecoles-9782212137002},
isbn = 2212137001,
x-equipes = {demons PROVAL EXT},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage}
}
@article{bobot14sttt,
topics = {team},
doi = {10.1007/s10009-014-0314-5},
hal_id = {hal-00967132},
hal = {http://hal.inria.fr/hal-00967132/en},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Let's Verify This with {Why3}},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
volume = 17,
number = 6,
pages = {709--727},
year = 2015,
note = {See also \url{http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html}},
publisher = {Springer Berlin / Heidelberg},
x-type = {article},
x-support = {revue},
x-cle-support = {STTT},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@inproceedings{filliatre14cav,
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
pages = {1--16},
crossref = {cav2014},
topics = {team},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
hal_id = {hal-00873187},
hal = {http://hal.archives-ouvertes.fr/hal-00873187/en/},
pdf = {http://hal.archives-ouvertes.fr/hal-00873187/PDF/main.pdf},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without any observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.
}
}
@article{gondelman16fmsd,
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
journal = {Formal Methods in System Design},
publisher = {Springer},
year = 2016,
volume = 48,
number = 3,
pages = {152--174},
issn = {1572-8102},
doi = {10.1007/s10703-016-0243-x},
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-01396864v1},
keywords = {Why3},
type_publi = {irevcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {revue},
x-editorial-board = {yes},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.
}
}
@inproceedings{cfmp14vstte,
hal = {http://hal.inria.fr/hal-01067197},
author = {Martin Clochard and Jean-Christophe
Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Formalizing Semantics with an Automatic Program
Verifier},
pages = {37--51},
crossref = {vstte14},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{cfp15vstte,
hal = {http://hal.inria.fr/hal-01162661},
author = {Martin Clochard and Jean-Christophe
Filli\^atre and Andrei Paskevich},
title = {How to avoid proving the absence of integer overflows},
pages = {94--109},
crossref = {vstte15},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@book{ProgrammerOCaml2014Eyrolles,
topics = {team},
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {Apprendre \`a programmer avec OCaml. Algorithmes et structures de donn\'ees},
publisher = {Eyrolles},
year = 2014,
month = sep,
pages = 429,
url = {https://usr.lmf.cnrs.fr/programmer-avec-ocaml/},
isbn = 9782212136784,
x-equipes = {demons PROVAL},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage},
hal = {http://hal.inria.fr/hal-01063853}
}
@inproceedings{filliatre14jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre},
title = {Le petit guide du bouturage, ou comment r\'ealiser des arbres mutables en {OCaml}},
crossref = {jfla14},
note = {\url{https://usr.lmf.cnrs.fr/~jcf/publis/bouturage.pdf}}
}
@article{filliatre14tangente,
author = {Jean-Christophe Filli\^atre},
title = {D\'emonstration. L'ordinateur \`a la rescousse},
journal = {Tangente (hors-s\'erie num\'ero 52)},
year = 2014,
number = 52,
pages = {34--36},
month = {February},
topics = {team,lri},
type_publi = {diffusion}
}
@inproceedings{pereira16jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {It\'erer avec confiance},
crossref = {jfla16},
hal = {https://hal.inria.fr/hal-01240891}
}
@inproceedings{pereira16nfm,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {A Modular Way to Reason About Iteration},
crossref = {nfm16},
abstract = { In this paper we present an approach to specify
programs performing iterations. The idea is to
specify iteration in terms of the nite sequence of
the elements enumerated so far, and only those. In
particular, we are able to deal with
non-deterministic and possibly innite iteration. We
show how to cope with the issue of an iteration no
longer being consistent with mutable data. We
validate our proposal using the deductive verication
tool Why3 and two iteration paradigms, namely
cursors and higher-order iterators. For each
paradigm, we verify several implementations of
iterators and client code. This is done in a modular
way, i.e., the client code only relies on the
specication of the iteration. },
hal = {https://hal.inria.fr/hal-01281759}
}
@inproceedings{filliatre16,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {Producing All Ideals of a Forest, Formally (Verification Pearl)},
crossref = {vstte16},
hal = {https://hal.inria.fr/hal-01316859}
}
@techreport{gondelman16reg,
topics = {team},
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {A Pragmatic Type System for Deductive Verification},
type = {Research Report},
institution = {Universit\'e Paris Sud},
year = 2016,
abstract = { In the context of deductive verication, it is customary
today to handle programs with pointers using either
separation logic, dynamic frames, or explicit memory
models. Yet we can observe that in numerous
programs, a large amount of code ts within the scope
of Hoare logic, provided we can statically control
aliasing. When this is the case, the code
correctness can be reduced to simpler verication
conditions which do not require any explicit memory
model. This makes verication conditions more
amenable both to automated theorem proving and to
manual inspection and debugging. In this paper, we
devise a method of such static aliasing control for
a programming language featuring nested data
structures with mutable components. Our solution is
based on a type system with singleton regions and
eects, which we prove to be sound.},
hal = {https://hal.archives-ouvertes.fr/hal-01256434v3},
note = {\url{https://hal.archives-ouvertes.fr/hal-01256434v3}}
}
@misc{cfpp17,
topics = {team},
author = {Arthur Chargu{\'e}raud and Jean-Christophe Filli{\^a}tre and
M{\'a}rio Pereira and Fran\c{c}ois Pottier},
title = {{VOCAL} -- {A} {V}erified {OC}aml {L}ibrary},
howpublished = {ML Family Workshop},
month = {September},
year = {2017},
hal = {https://hal.inria.fr/hal-01561094}
}
@inproceedings{fpds18jfla,
topics = {team},
crossref = {jfla18},
title = {V{\'e}rification de programmes fortement imp{\'e}ratifs avec {W}hy3},
author = {Jean-Christophe Filli{\^a}tre and M{\'a}rio Pereira and
Sim{\~a}o Melo de Sousa},
hal = {https://hal.inria.fr/hal-01649989},
pdf = {https://hal.inria.fr/hal-01649989/file/main.pdf},
hal_id = {hal-01649989},
hal_version = {v2}
}
@techreport{fgpps18,
author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and
Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa},
title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml
{P}rograms},
hal = {https://hal.inria.fr/hal-01783851},
pdf = {https://hal.inria.fr/hal-01783851/file/main.pdf},
note = {artifact: \url{https://www.lri.fr/~mpereira/correct_ocaml.ova}},
year = {2018}
}
@inproceedings{gospelfm19,
topics = {team},
crossref = {fm19},
author = {Arthur Chargu\'eraud and Jean-Christophe Filli\^atre and Cl\'audio Belo Louren\c{c}o and M\'ario Pereira},
title = {{GOSPEL} --- Providing {OCaml} with a Formal Specification Language},
hal = {https://hal.inria.fr/hal-02157484}
}
@book{NSIPremiere2019Ellipses,
author = {Thibaut Balabonski and Sylvain Conchon and Jean-Christophe Filli\^atre and Kim Nguyen},
title = {Num\'erique et Sciences Informatiques, 30 le\c{c}ons avec exercices corrig\'es},
publisher = {Ellipses},
year = 2019,
month = aug,
pages = 528,
url = {http://www.nsi-premiere.fr},
isbn = 9782340033641,
x-equipes = {demons PROVAL},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage}
}
@misc{filliatre15mathematicpark,
author = {Jean-Christophe Filli\^atre},
title = {V\'erification d\'eductive de programmes},
howpublished = {Mathematic Park, Institut Henri Poincar\'e},
url = {https://www.youtube.com/watch?v=Jf5TYvpkXuc},
year = 2015,
month = mar,
note = {S\'eminaire invit\'e},
topics = {team, lri},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {diffusion},
x-scientific-popularization = {yes},
x-invited-conference = {yes}
}
@misc{filliatre18msp,
author = {Jean-Christophe Filli\^atre},
title = {An Introduction to Deductive Program Verification},
howpublished = {Mathematical Summer in Paris (summer school)},
year = 2018,
month = jul,
note = {Cours invit\'e},
topics = {team, lri},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {diffusion},
x-international-audience = {yes},
x-invited-conference = {yes}
}
@misc{filliatre18sem-pour-tous,
author = {Jean-Christophe Filli\^atre},
title = {Parcours d'un informaticien},
howpublished = {S\'eminaire Info Pour Tous},
url = {https://www.youtube.com/watch?v=LPvZqZV5LKA},
year = 2018,
month = sep,
address = {Paris, France},
note = {S\'eminaire invit\'e},
topics = {team, lri},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {diffusion},
x-invited-conference = {yes}
}
@misc{filliatre17diderot,
author = {Jean-Christophe Filli\^atre},
title = {V\'erification d\'eductive de programmes},
howpublished = {S\'eminaire Acqu\'erir une culture commune
dans le domaine de l'informatique, lyc\'ee Diderot, Paris},
year = 2017,
month = may,
note = {S\'eminaire invit\'e},
topics = {team, lri},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {diffusion},
x-invited-conference = {yes}
}
@inproceedings{filliatre19jfla,
author = {Jean-Christophe Filli\^atre},
title = {Retour sur 25 ans de programmation avec {OCaml}},
crossref = {jfla19},
note = {S\'eminaire invit\'e},
hal = {https://hal.inria.fr/hal-02406208},
topics = {team, lri},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {diffusion},
x-invited-conference = {yes}
}
@inproceedings{filliatre18itp,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification},
crossref = {itp2018},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre18fide,
author = {Jean-Christophe Filli\^atre},
title = {Auto-active verification using {Why3}'s {IDE}},
booktitle = {4th Workshop on Formal Integrated Development Environment},
year = 2018,
month = jul,
address = {Oxford, UK},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre17keysymposium,
author = {Jean-Christophe Filli\^atre},
title = {{Why3} --- where programs meet provers},
booktitle = {KeY Symposium 2017},
year = 2017,
month = oct,
address = {Rastatt, Germany},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre17verifythis,
author = {Jean-Christophe Filli\^atre},
title = {{Why3} Tutorial},
booktitle = {VerifyThis 2017},
year = 2017,
month = apr,
address = {Uppsala, Sweden},
note = {Invited tutorial},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre17framacsparkday,
author = {Jean-Christophe Filli\^atre},
title = {The {Why3} tool for deductive verification and verified {OCaml} libraries},
booktitle = {Frama-C \& SPARK Day 2019},
year = 2019,
month = jun,
address = {Paris, France},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre14msc,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification with {Why3}},
booktitle = {Mathematical Structures of Computation --- Formal Proof, Symbolic Computation and Computer Arithmetic},
year = 2014,
month = feb,
address = {Lyon, France},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre13msr,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification with {Why3}},
booktitle = {MSR-Inria Joint Centre ``Spring Day''},
year = 2013,
month = may,
address = {Lyon, France},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre19ifm,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Verification of {OCaml} Libraries},
booktitle = {15th International Conference on integrated Formal Methods},
year = 2019,
month = dec,
address = {Bergen, Norway},
note = {Invited talk},
topics = {team, lri},
hal = {https://hal.inria.fr/hal-02406253},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre20jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre},
title = {Mesurer la hauteur d'un arbre},
crossref = {jfla20},
topics = {team},
note = {\url{https://usr.lmf.cnrs.fr/~jcf/hauteur/}},
x-slides = {https://usr.lmf.cnrs.fr/~jcf/hauteur/pres-hauteur.pdf},
hal = {https://hal.inria.fr/hal-02315541}
}
@techreport{becker20rr,
topics = {team},
title = {Rapport d'avancement sur la v{\'e}rification formelle des algorithmes de {ParcourSup}},
author = {Becker, Benedikt and Filli{\^a}tre, Jean-Christophe and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-02447409},
type = {Technical Report},
institution = {Universit{\'e} Paris-Saclay},
year = 2020,
month = jan
}
@article{filliatre20jlamp,
author = {Jean-Christophe Filli\^atre},
title = {Simpler Proofs with Decentralized Invariants},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = 121,
publisher = {Elsevier},
year = 2021,
topics = {team},
month = jan,
note = {See \url{https://usr.lmf.cnrs.fr/~jcf/spdi/}},
hal = {https://hal.inria.fr/hal-02518570},
doi = {https://doi.org/10.1016/j.jlamp.2021.100645}
}
@inproceedings{paskevich20isola,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Abstraction and Genericity in {Why3}},
booktitle = {9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},
month = oct,
year = 2020,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 12476,
pages = {122--142},
editor = {Tiziana Margaria and Bernhard Steffen},
address = {Rhodes, Greece},
topics = {team},
note = {See also \url{https://usr.lmf.cnrs.fr/~jcf/isola-2020/}},
hal = {https://hal.inria.fr/hal-02696246}
}
@inproceedings{filliatre20coqworkshop,
author = {Jean-Christophe Filli\^atre},
title = {A {Coq} retrospective - at the heart of {Coq} architecture, the genesis of version 7.0},
booktitle = {The Coq Workshop 2020},
year = 2020,
month = {July},
address = {virtual},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes},
hal = {https://hal.inria.fr/hal-02890460},
url = {https://www.youtube.com/watch?v=tROOcO44Uho#t=64.5m}
}
@book{balabonski20book,
topics = {team},
title = {Num{\'e}rique et Sciences Informatiques, 24 le\c{c}ons avec exercices corrig{\'e}s. Terminale},
author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim},
hal = {https://hal.inria.fr/hal-03023099},
publisher = {Ellipses},
year = 2020
}
@inproceedings{filliatrepascutto21,
author = {Jean-Christophe Filli\^atre and Cl\'ement Pascutto},
title = {{Ortac}: Runtime Assertion Checking for {OCaml}},
year = 2021,
topics = {team},
booktitle = {Proceedings of the 21st International Conference on Runtime Verification (RV'21)},
month = may,
hal = {https://hal.inria.fr/hal-03252901},
abstract = {Runtime assertion checking (RAC) is a convenient set of
techniques that lets developers abstract away the
process of verifying the correctness of their
programs by writing formal specifications and
automating their verification at runtime. In this
work, we present ortac, a runtime assertion checking
tool for OCaml libraries and programs. OCaml is a
functional programming lan- guage in which idioms
rely on an expressive type system, modules, and
interface abstractions. ortac consumes interfaces
annotated with type invariants and function
contracts and produces code wrappers with the same
signature that check these specifications at
runtime. It provides a flexible framework for
traditional assertion checking, monitoring mis-
behaviors without interruptions, and automated fuzz
testing for OCaml programs. This paper presents an
overview of ortac features and highlights its main
design choices.}
}
@techreport{vocalCRfinal2021,
topics = {team},
author = {Jean-Christophe Filli\^atre},
title = {Compte-rendu de fin de projet ANR-15-CE25-0008 ``VOCaL''},
institution = {Laboratoire M\'ethodes Formelles},
year = 2021,
month = jun,
hal = {https://hal.inria.fr/hal-03326775}
}
@inproceedings{filliatre21rv,
topics = {team},
title = {{Ortac}: Runtime Assertion Checking for {OCaml}},
author = {Filli{\^a}tre, Jean-Christophe and Pascutto, Cl{\'e}ment},
hal = {https://hal.inria.fr/hal-03252901},
booktitle = {21st International Conference on Runtime Verification},
year = 2021
}
@inproceedings{filliatre22rv,
topics = {team},
title = {Optimizing Prestate Copies in Runtime Verification of Function Postconditions},
author = {Filli{\^a}tre, Jean-Christophe and Pascutto, Cl{\'e}ment},
hal = {https://hal.inria.fr/hal-03690675v1},
booktitle = {22nd International Conference on Runtime Verification},
year = 2022
}
@misc{VerifyThis2021DLLtoBST,
title = {Solution to VerifyThis 2021 challenge 2},
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
year = {2021},
note = {\url{https://toccata.gitlabpages.inria.fr/toccata/gallery/verifythis_2021_dll_to_bst.en.html}}
}
@book{balabonski22book,
topics = {team},
title = {Informatique - {MP2I/MPI} - {CPGE} 1re et 2e ann{\'e}es - {Cours} et exercices corrig{\'e}s},
author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim and Sartre, Laurent},
hal = {https://hal.inria.fr/hal-03886751},
publisher = {Ellipses},
year = 2022
}
@book{balabonski19book,
topics = {team},
title = {Num{\'e}rique et Sciences Informatiques, 30 le{\c c}ons avec exercices corrig{\'e}s. {Premi{\`e}re.}},
author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim},
hal = {https://inria.hal.science/hal-02379073},
publisher = {Ellipses},
year = 2019
}
@inproceedings{filliatre23jfla,
topics = {team},
title = {L'arithm{\'e}tique de s{\'e}paration},
author = {Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03886759},
booktitle = {JFLA 2023 - 34{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Timothy Bourke and Delphine Demange},
pages = {274--283},
year = 2023
}
@proceedings{icfem04,
title = {Formal Engineering Methods},
year = 2004,
booktitle = {6th International Conference on Formal Engineering Methods},
series = {Lecture Notes in Computer Science},
volume = 3308,
editor = {Jim Davies and Wolfram Schulte and Mike Barnett},
address = {Seattle, WA, USA},
month = nov,
publisher = {Springer}
}
@proceedings{cav07,
editor = {Werner Damm and Holger Hermanns},
title = {Computer Aided Verification},
booktitle = {19th International Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4590,
address = {Berlin, Germany},
month = jul,
year = {2007}
}
@proceedings{cav2014,
editor = {Armin Biere and Roderick Bloem},
title = {Computer Aided Verification},
booktitle = {26th International Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8859,
address = {Vienna, Austria},
month = jul,
year = 2014
}
@proceedings{jfla05,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2005,
booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = mar,
publisher = {INRIA}
}
@proceedings{jfla06,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2006,
booktitle = {Dix-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla07,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2007,
booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla08,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2008,
booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla09,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2009,
booktitle = {Vingti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Saint-Quentin sur Is\`ere},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla10,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2010,
booktitle = {Vingt-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Vieux-Port La Ciotat, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla11,
title = {Journ\'ees Francophones des Langages Applicatifs},
editor = {Sylvain Conchon},
year = 2011,
booktitle = {Vingt-deuxi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {La Bresse, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla13,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2013,
booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
month = feb,
address = {Aussois, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla14,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2014,
booktitle = {Vingt-cinqui\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Fr\'ejus, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla16,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2016,
booktitle = {Vingt-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Saint-Malo, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla18,
topics = {team},
title = {Vingt-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Banyuls-sur-mer, France},
year = 2018,
month = jan,
editor = {Boldo, Sylvie and Magaud, Nicolas},
hal = {https://hal.inria.fr/hal-01707376}
}
@proceedings{jfla19,
title = {Trenti\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trenti\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Les Rousses, France},
year = 2019,
month = jan,
editor = {Magaud, Nicolas and Dargaye, Zaynah},
hal = {https://hal.archives-ouvertes.fr/hal-01985195v1}
}
@proceedings{jfla20,
title = {Trente-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trente-et-uni\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Gruissan, France},
year = 2020,
month = jan,
editor = {Dargaye, Zaynah and R\'egis-Gianas, Yann}
}
@proceedings{esop08,
title = {17th European Symposium on Programming (ESOP'08)},
booktitle = {17th European Symposium on Programming (ESOP'08)},
year = 2008,
address = {Budapest, Hungary},
month = apr
}
@proceedings{postfoveoos11,
editor = {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7421,
year = 2012,
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {FOVEOOS}
}
@proceedings{vstte12,
booktitle = {Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE)},
month = jan,
year = 2012,
address = {Philadelphia, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
series = {Lecture Notes in Computer Science},
volume = 7152,
publisher = {Springer}
}
@proceedings{cade13,
title = {24th International Conference on Automated Deduction},
booktitle = {24th International Conference on Automated Deduction (CADE-24)},
address = {Lake Placid, USA},
month = {June},
year = 2013,
series = {Lecture Notes in Artificial Intelligence},
volume = 7898,
publisher = {Springer}
}
@proceedings{vstte13,
booktitle = {Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE)},
month = may,
year = 2013,
address = {Atherton, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Ernie Cohen and Andrey Rybalchenko},
series = {Lecture Notes in Computer Science},
volume = {8164},
publisher = {Springer}
}
@proceedings{vstte14,
booktitle = {6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2014,
address = {Vienna, Austria},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Dimitra Giannakopoulou and Daniel Kroening},
series = {Lecture Notes in Computer Science},
volume = 8471,
publisher = {Springer}
}
@proceedings{vstte15,
booktitle = {7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2015,
address = {San Francisco, California, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Arie Gurfinkel and Sanjit A. Seshia},
series = {Lecture Notes in Computer Science},
volume = 9593,
publisher = {Springer}
}
@proceedings{vstte16,
booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2016,
address = {Toronto, Canada},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Sandrine Blazy and Marsha Chechik},
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
@proceedings{itp2018,
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8},
doi = {10.1007/978-3-319-94821-8},
isbn = {978-3-319-94820-1}
}
@proceedings{nfm16,
booktitle = {8th NASA Formal Methods Symposium},
address = {Minneapolis, MN, USA},
audience = {internationale},
year = 2016,
month = jun,
editor = {Rayadurgam, Sanjai and Tkachuk, Oksana},
series = {Lecture Notes in Computer Science},
volume = {9690},
publisher = {Springer}
}
@proceedings{fm19,
title = {FM 2019 23rd International Symposium on Formal Methods},
booktitle = {FM 2019 23rd International Symposium on Formal Methods},
month = oct,
year = 2019,
address = {Porto, Portugal},
editor = {Annabelle McIver and Maurice ter Beek}
}