filliatre.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc filliatre.cite -ob filliatre.bib -c 'author : "Filli\^atre" and topics : "team"' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/biblio/crossrefs.bib}}
@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}
}
@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}
}
@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},
  title = {{Formal Verification of Floating-Point Programs}},
  booktitle = {18th IEEE International Symposium on Computer Arithmetic},
  pages = {187-194},
  month = jun,
  year = 2007,
  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 = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  abstract = {
  This paper introduces a methodology to perform formal verification
  of floating-point C programs. It extends an existing tool for the
  verification of C programs, Caduceus, with new annotations specific
  to floating-point arithmetic. The Caduceus first-order logic model
  for C programs is extended accordingly. Then verification conditions
  expressing the correctness of the programs are obtained in the usual
  way and can be discharged interactively with the Coq proof
  assistant, using an existing Coq formalization of floating-point
  arithmetic.  This methodology is already implemented and has been
  successfully applied to several short floating-point programs, which
  are presented in this paper.}
}
@inproceedings{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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/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.
}
}
@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 = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  abstract = { The problem of disjoint sets, also known as union-find,
  consists in maintaining a partition of a finite set within a data
  structure. This structure provides two operations: a function find
  returning the class of an element and a function union merging two
  classes. An optimal and imperative solution is known since 1975.
  However, the imperative nature of this data structure may be a
  drawback when it is used in a backtracking algorithm. This paper
  details the implementation of a persistent union-find data structure
  as efficient as its imperative counterpart.  To achieve this result,
  our solution makes heavy use of imperative features and thus it is a
  significant example of a data structure whose side effects are
  safely hidden behind a persistent interface.  To strengthen this
  last claim, we also detail a formalization using the Coq proof
  assistant which shows both the correctness of our solution and its
  observational persistence. },
  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 = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf},
  url = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf},
  abstract = {  This functional pearl proposes an ML implementation of
  the Garsia--Wachs algorithm.
  This somewhat obscure algorithm builds a binary tree with minimum
  weighted path length from weighted leaf nodes given in symmetric
  order. Our solution exhibits the usual benefits of functional
  programming (use of immutable data structures, pattern-matching,
  polymorphism) and nicely compares to the purely imperative
  implementation from \emph{The Art of Computer Programming}.},
  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},
  title = {{Semi-Persistent Data Structures}},
  crossref = {esop08},
  year = 2008,
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/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}
}
@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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  x-equipes = {demons PROVAL EXT},
  x-type = {articlecourt},
  x-support = {actes},
  x-cle-support = {CAV}
}
@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 = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz},
  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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/sos.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/sos.pdf},
  code = {http://www.lri.fr/~filliatr/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{http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}},
  month = mar,
  year = 2003,
  url = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/jphd.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.pdf},
  type_publi = {irevcomlec},
  topics = {team}
}
@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 = {http://www.lri.fr/~filliatr/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 = {http://www.lri.fr/~filliatr/publis/enum2.pdf},
  url = {http://www.lri.fr/~filliatr/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 = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf},
  abstract = {
  Cet article pr\'esente une r\'ealisation en Ocaml de la structure de
  cordes introduite par Boehm, Atkinson et Plass. Nous montrons
  notamment comment cette structure de donn\'ees s'\'ecrit naturellement
  comme un foncteur, transformant une structure de s\'equence en une
  autre structure de m\^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,
  note = {\url{http://knuth07.labri.fr/exposes.php}},
  address = {Bordeaux, France},
  month = {October},
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-pdf = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  abstract = {We introduce a methodology to formally verify MIX programs.
  It consists in annotating a MIX program with logical annotations
  and then to turn it into a set of purely sequential programs on
  which classical techniques can be applied.
  Contrary to other approaches of verification of unstructured
  programs, we do not impose the location of annotations but only the
  existence of at least one invariant on each cycle in the control
  flow graph. A prototype has been implemented and used to verify
  several programs from \emph{The Art of Computer Programming}.},
  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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/find.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/fpp.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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}
}
@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}
}
@inproceedings{mlpost09jfla,
  author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
  title = {{Faire bonne figure avec Mlpost}},
  url = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/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 = {Proceedings of the First Interactive Theorem Proving Conference},
  year = 2010,
  series = {LNCS},
  address = {Edinburgh, Scotland},
  month = jul,
  publisher = {Springer},
  editor = {Matt Kaufmann and Lawrence C. Paulson},
  volume = {6172},
  pages = {147--162},
  hal = {http://hal.inria.fr/inria-00450789/},
  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 = {http://www.lri.fr/~filliatr/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}
}
@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://www.lri.fr/~filliatr/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.lri.fr/}}
}
@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.lri.fr/download/manual-0.81.pdf},
  note = {\url{http://why3.lri.fr/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.lri.fr/download/manual-0.82.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.82.pdf}},
  hal = {}
}
@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.lri.fr/download/manual-0.86.1.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.86.1.pdf}},
  hal = {}
}
@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 = {http://www.lri.fr/~filliatr/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}
}
@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 = {http://www.lri.fr/~filliatr/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 = {http://www.lri.fr/~filliatr/pub/compare2012.pdf}
}
@inbook{filliatre12ejcp,
  author = {Jean-Christophe Filli\^atre},
  title = {Course notes EJCP 2012},
  chapter = {V\'erification d\'eductive de programmes avec Why3},
  topics = {team},
  keywords = {Why3},
  x-equipes = {demons PROVAL},
  x-support = {diffusion},
  x-type = {invitation},
  month = jun,
  year = 2012,
  rawebnote = {\url{http://why3.lri.fr/ejcp-2012/}},
  pdf = {http://why3.lri.fr/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://proval.lri.fr/publications/bobot12icfem.pdf}
}
@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{http://www.lri.fr/~filliatr/combine/}},
  hal = {http://hal.inria.fr/hal-00779431},
  url = {http://www.lri.fr/~filliatr/pub/jfla-2013.pdf}
}
@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://www.lri.fr/~marche/DigiCosmeSchool/filliatre.html}}
}
@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.lri.fr/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  hre.
  }
}
703tic6-0243-x
  title = {The Spirit ocolcomlec},
  x-intesl-00873187/en/},
  pdf = {},
  pdf = {},
  pages = {1--20},
  topics = {team,lri},
  keywords = ger Berlin / Heidelberg},
  volume = 13,
  numa>},
  year = 2013,
  topiertes.fr/hal-00873187/PDF/main.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 specifica.
  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 bcfmp14://hal.inria.fr/hal-00809651/en/">http://hal.inria.fr/hacfmp14://hal.cfmp14://ha13Eyrolles">
@book{http://hal.inria.fr/hal-00967132/en},
  author = {FraFn toolsrograally vercharged uAial case Pfolklore a>,
  ates in Computer37--= {Stev://hal.inria.fr/hal-008753954/a>},
  ich},
  title = {The Spication Changes},
  crossref = {vstte13},
  pages = {191--201},
  topics = {team,lri},
  keywords = {Why3},
  typecfp15://hal.inria.fr/hal-00809651/en/">http://hal.inria.fr/hacfp15://hal.cfp15://ha13Eyrolles">
@book{http://67132/en},
  author = {Fraon is eavoidcations/ror an
  -Source},
 2015uthorifi">http://hal.inria.fr/hal-008753955/a>},
  5ch},
  title = {The Spication Changes},
  crossref = {vstte13},
  pages = {191--201},
  topics = {team,lri},
  keywords = {Why3},
  typeauthor =er= {Jekevi  \url{https://www.lri.fr/~marche/DigiCosmeSchool/author =er= {Jekevi  \url{httauthor =er= {Jekevi  \url{he}
}
http://">
@inproceedings{
@book{

bol
@inproce\"el Courant anonchr@inp en   tyiagrammingnd R\'emy El Siba\"{\i}e},
6 title 6es.com/Sccolcomlec},
  x-intesl-00873ilippa Gardner124089note = sl-00873ilippa Gardner124089n = {yes},
  hal = {http://inforum.org.pt/INForum2012/docpnproce16nf/20pnproce16nf/e}
}
bol
@inproce\"el Courant aA ModsysteWayis el Reso AbficaIttware vmmingnd R\'emy El Siba\"{\inf/
6 tnf/
6hives-ouvertes.fr/halorous defort = nd there arehttpwwoare s ee intro
                  
  x-typeber of ns/rittware vsses tnnot ptions annnnnnnnnnnnnnnnne introduttware vmulatermtre and Anfinethe whcions foooooooooooooooootatioela and eure oericaso f sen">boon fromtex  ar
                  
 in the senw tend ormal238-eolcharg
                   aredp (P nsiroof ">bontesistamulnfineuttware vSMT  annnnnnnnnnnnnnnnnehn ihn is ecops part
tatiissuourceentsttware vmns annnnnnnnnnnnnnnnnlo 2015bens/r  tracte arnd few formalt coSMT  annnnnnnnnnnnnnnnnvooldatioco a Novemolcutions to f">http://v Fillthis
    ooooooooooooootucti3esop is iwotsttware vmdes-digplated
  f
    oooooooooooooocursor this higoir some isttware numFn ioncg
                  des-digpenw tnditions that cs a simple numsons fooooooooooooooooosttware nthis clien.

  In T progra14neon a nmodsyst fooooooooooooooooowaatei.e.te andclien.

  Ioon frr{Pisal
  spe annnnnnnnnnnnnnnnne intal.lri.fr/tatiittware vSMom/Sccolcomlec},
  x-intesl-00873ilippa Gardner1281759ote = sl-00873ilippa Gardner1281759{

bol
@inproce\"el Courant aPFEM},ionsAll I-eolabstracFn es {Wapoints i(^a}tre and Jorons )>http://hal.inria.fr/hal-008753956/a>},
  6es.com/Sccolcomlec},
  x-intesl-00873ilippa Gardner1316859ote = sl-00873ilippa Gardner1316859{

bo'e and Guillaume Melquio3-odelcport = {actes},
  x-equipes = {dA Pfag case T8221reliabl  Inhe Filli{\^a}tre and J/a>},
  i= {de Rh{\^o}ne-Alpes / LIP LaboratoireProgram Vétoire  ,
  year Software 6his ertes.fr/halorous 7/PDF/main.pdf">http://v Fillthis, Thissocusal crf
    ooooooooooooootodayis ehlcpe is surprrchargeenginmposram as a set annnnnnnnnnnnnnnnnestract = {This , dyw.l~B
 rodulatn ioxplicThiheserf
    ooooooooooooooto dinumYeriodhe pu.
  Ghe  abstrndure of g
                  
  x-typ,s a rich amounted 

  Iotrchargam that cops
                  d 
Hoend This , ation= {
odhe puizatge them. bstra
                  oolaam a.illin C program toical, prove co
    ooooooooooooooc},
  abe purpor">htion cof
  ghr/v Fillthis
    ooooooooooooooorrespondinasure do ghosryes}jar">yioxplicThiheserf
    ooooooooooooooto din T promlogy v Fillthisoorrespondinsero
    ooooooooooooooodunormalg-poinourpose is
  to benefit  Coq) dons annnnnnnnnnnnnnnnn1.pdf" LIPpecs and is debuggm a.irous defort =enw  annnnnnnnnnnnnnnnnd},
se pages = { of plemizatge oolaam a  abstractot annnnnnnnnnnnnnnnnais surprisingly subtle focussingnt Indlt co annnnnnnnnnnnnnnnneue pouraitnd few formalser-dn and. Oo ae},
  absig
                  nsert logicL-style programmit proetoout aifferenc
                  elanguage
  wctions tos ensussche.rit ocolcomlec},
  x-intesl-00873187/en/},
  pdf = {},
  pdf = {},
  pdf = {http://hal.inria.fr/hacfpp17ypcfpp17e}
}
CAO Mos\'e > @inproceeding {, 6tle = {Separation Predicates: a Taste Ef Separation Logic yeargs of the 22nd European Symposium on Programmingwith {Why33ammatiive PrograJim ntregular dWol rodram ultar">boldka narnetpes / -conferenceSfocton aWAe = {iuel d'algorinovming}, month = mar, yegiCosme} Spring Schocav07 the use of Whtional-audience = {yes}, x-editorcav07 tcav07e} } },li\^atre}, t9tle = {Separation Predicates: aposium onAn= { ^a}tre and J/a>},}, month = mar, year =gs of the 22nd European Symposium on Programmingwith {Why4590s / -conference, no,e MaThe iuel d'algorijule = {{ARMY} fo07egiCosme} Spring Schocavndrei he use of Whtional-audience = {yes}, x-editorcavndrei Paskevich}, },li\^atre}, 26tle = {Separation Predicates: aposium onAn= { ^a}tre and J/a>},}, month = mar, year =gs of the 22nd European Symposium on Programmingwith {Why8859s / -conferenceVrogna, A. iaiuel d'algorijule = {{ARMY}kevigiCosme} Spring Schoitle05i he use of Whtional-audience = {yes}, x-editoritle05i itle05e} } },li\^atre}, Seizi\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programs Meet }, month = de l'giCosme} Spring Schoitle06i he use of Whtional-audience = {yes}, x-editoritle06 title06e} } },li\^atre}, Dix-estti\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet }, month = de l'giCosme} Spring Schoitle07 the use of Whtional-audience = {yes}, x-editoritle07 title07e} } },li\^atre}, Dix-huiti\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet }, month = de l'giCosme} Spring Schoitle08 the use of Whtional-audience = {yes}, x-editoritle08 title08e} } },li\^atre}, Dix-neuvi\`e}hemmMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet }, month = de l'giCosme} Spring Schoitle09 the use of Whtional-audience = {yes}, x-editoritle09 title09e} } },li\^atre}, V-auti\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet -conferenceSaint-Q why3n-the Is\`eramming}, month = de l'Infoa>}, pages = {191--201}, }, year a>}, year = 2013, topics{team,lri}, keywords = {Why3}, typeitle 0 the use of Whtional-audience = {yes}, x-editoritle 0 title 0e} } },li\^atre}, V-aut-et-uni\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet -conferenceVroux-Pux-gLa Ciform,ion; Romming}, month = de l'Infoa>}, pages = {191--201}, }, year a>}, year = 2013, topics{team,lri}, keywords = {Why3}, typeitle 1 the use of Whtional-audience = {yes}, x-editoritle 1 title 1e} } h year Software11a>},li\^atre}, V-aut-douxi\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet -conferenceLa Bnfere,ion; Romming}, month = de l'Infoa>}, pages = {191--201}, }, year a>}, year = 2013, topics{team,lri}, keywords = {Why3}, typeitle 3 the use of Whtional-audience = {yes}, x-editoritle title = {{C },li\^atre}, V-aut--Chrri\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programfebeet -conferenceA. sot, Fon; Romminga>}, pages = {191--201}, }, year a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, onal-audience = {yes}, xJFLl'giCosme} Spring Schoitle16i he use of Whtional-audience = {yes}, x-editoritle 6 title 6es.c },li\^atre}, V-aut-estti\`e}hemMarch/hatoion; R-00onaithfsean-Cet prApp {}, fc year Programjaneet -conferenceSaint-Malo Fon; Romminga>}, pages = {191--201}, }, year a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, onal-audience = {yes}, xJFLl'giCosme} Spring Schoa na08 the use of Whtional-audience = {yes}, x-editora na08 ta na08es.c },li\^atre}, t7ogr Paskevich}, title = {Why3 --- (mlec'08)/a>}, Software08a>},-conference,udapes {WHu-Cer iuel d'algoriapres}, hal = {http://proval.yearerence on B prch\'Bcompr/hal.iFerrucciohDprianifilliath MosGPasv author = {FraFn too = {Jean-Chris\'e aj2nd-Oli\^tauthor = {J, R}, seuthel2nd Melrt =s Phere averibligae = {Separation Predicate{WapVeOOSTofan and li\^atre}, Fn too = {Jean-Chris\'e aj2nd-Oli\^tauthor = {J, R}, seuthel2nd Melrt =s Phere averibligae = {Separation Predicate{WapVeOOSTofan and }, month = mar, year =gs of the 22nd European Symposium on Programmingwith {Why7421year Software1ter Science}, publisher = {Springer}, address = {Kyoto, Japan}, words = {Why3}, type_publi = {icolcoFOVEOOS'giCosme} Spring Scho>}, 2pdhe use of Whtional-audience = {yes}, x-editor>}, 2pd>}, 2val.yearli\^atre}, V>, author = {J:2boogiiulatPaske,e Fillia and (itle = {Separation PredicatesVSTTE) year Programjaneet e Reeves and Elvinia Riccobhiladelphype = {ier Science}, publisher = {Springer}, a a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, type_publi = {icolcoVSTTE yearerence on RajeevmMantrerkshop (PLM{\"u}7, elcport = ahtPo dinkiear =gs of the 22nd European Symposium on Programmingwith {Why7152ming}, month = mar, yegiCosme} Spring Schocahor = he use of Whtional-audience = {yes}, x-editorcahor = {Jean-Chriauthor = {Fra2itle = {Separation Predicates: an Numericahe Fill J/a>},li\^atre}, 2itle = {Separation Predicates: an Numericahe Fill J (CADE-24)es / -conferenceLakeorgecide = {iuel d'algori{JuB and Z Software13a>},gs of the 22nd European SymAm,leanite ofte}, gogrammingwith {Why7898ming}, month = mar, yegiCosme} Spring Scho875395}, }, titleyearli\^atre}, V>, author = {J:2boogiiulatPaske,e Fillia and (5tle = {Separation PredicatesVSTTE) year Programmaynd Z Software13a>},-conferenceA settis, = {ier Science}, publisher = {Springer}, a a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, type_publi = {icolcoVSTTE yearerence on ErniJeanhedelcport = y Rybalchedkoear =gs of the 22nd European Symposium on Programmingwith {Why{8164 and }, month = mar, yegiCosme} Spring Scho875395ei he use of Whtional-audience = {yes}, x-editor8753954/a>}, ich},yearli\^atre}, 6tle^atr-- Predicates: aV>, author = {J:2boogiiulatPaskeelcpo Fillia and (VSTTE) year Programjule = {{ARMY}kevis / -conferenceVrogna, A. iaiuel cience}, publisher = {Springer}, a a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, type_publi = {icolcoVSTTE yearerence on Dimed ( G Monakopouloufilliaaniel Kroeolution: gs of the 22nd European Symposium on Programmingwith {Why8471and }, month = mar, yegiCosme} Spring Scho8753955i he use of Whtional-audience = {yes}, x-editor8753955/a>}, 5ch},yearli\^atre}, 7tle^atr-- Predicates: aV>, author = {J:2boogiiulatPaskeelcpo Fillia and (VSTTE) year Programjule = {{ARMY}kev5eet -conferenceSanFon; RiscoAL}, x-type = {iuel cience}, publisher = {Springer}, a a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, type_publi = {icolcoVSTTE yearerence on AiiusGPafinkel ttp://njit A.thentraion: gs of the 22nd European Symposium on Programming}, month = mar, yegiCosme} Spring Scho8753956i he use of Whtional-audience = {yes}, x-editor8753956/a>}, 6es.cyearli\^atre}, 8tle^atr-- Predicates: aV>, author = {J:2boogiiulatPaskeelcpo Fillia and (VSTTE) year Programjule = {{ARMY}kev6eet -conferenceTorProoAL},nadaiuel cience}, publisher = {Springer}, a a>}, year = 2013, topics{team,lri}, keywooles-978221213am,lri}, keywords = {Why3}, type_publi = {icolcoVSTTE yearerence on //ndrlowsBlazy00880268sha Chechikion: gs of the 22nd European Symposium on Programming}, month = mar, yegiCosme} Spring Schonf/ 6 the use of Whtional-audience = {yes}, x-editornf/ 6 tnf/ 6hiveyearli\^atre}, 8tleNASA -procics = {go)h}, tites / -conferenceMinneapolt, FMNe = {iuel sher = {Sprience}, publ and Z Software16year Programjunyearerence on Rayadurgeman//njarerkshTkachuk, Oks,naear =gs of the 22nd European Symposium on Programmingwith {Why{9690mming}, month = mar, yegiCosme} Sp