complete-other.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc complete-other.cite -ob complete-other.bib -c 'topics : "team" and $type<>"book" and $type<>"inbook" and $type<>"incollection" and $type<>"article" and $type<>"inproceedings" and $type<>"phdthesis" and $type<>"techreport" and year>=2004' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@manual{CoqManualV8,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version V8.0}},
year = 2004,
month = apr,
url = {http://coq.inria.fr},
note = {\url{http://coq.inria.fr}},
topics = {team,lri},
type_publi = {manuel}
}
@manual{CoqTutorialV8,
author = {G. Huet and G. Kahn and Ch. Paulin-Mohring},
title = {The {\sf Coq} Proof Assistant - A tutorial - Version 8.0},
month = apr,
year = 2004,
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel}
}
@manual{CoqManualV89,
author = {The {Coq} Development Team},
title = {The {Coq} Proof Assistant Reference Manual -- Version V8.9},
year = 2019,
note = {\url{http://coq.inria.fr}},
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion}
}
@mastersthesis{ayache05master,
author = {Nicolas Ayache},
title = {Coop\'eration d'outils de preuve interactifs et automatiques},
school = {Universit{\'e} Paris 7},
year = 2005,
topics = {team},
type_publi = {rapport},
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@mastersthesis{iguernelala09master,
author = {Mohamed Iguernelala},
title = {{Extension modulo Associativit\'e-Commutativit\'e
de l'algorithme de cl\^oture par congruence CC(X)}},
school = {Universit{\'e} Paris-Sud},
year = 2009,
topics = {team},
type_publi = {rapport},
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@mastersthesis{bardou07master,
author = {Romain Bardou},
title = {Invariants de classe et syst\`emes d'ownership},
school = {Master Parisien de Recherche en Informatique},
topics = {team},
type_publi = {rapport},
type_digiteo = {no},
year = 2007,
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport},
x-pdf = {http://romain.bardou.fr/papers/stage2007r.pdf},
url = {http://romain.bardou.fr/papers/stage2007r.pdf}
}
@mastersthesis{bertails06master,
author = {Alexandre Bertails},
title = {Langages synchrones avec horloges p\'eriodiques},
school = {Master Parisien de Recherche en Informatique},
month = sep,
year = 2006,
topics = {team},
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport},
x-pdf = {http://www.lri.fr/~bertails/misc/master_thesis.pdf},
url = {http://www.lri.fr/~bertails/misc/master_thesis.pdf}
}
@mastersthesis{kanig07master,
author = {Johannes Kanig},
title = {Certifying a Congruence Closure algorithm in {Coq} using Traces},
school = {Technische Universit\"at Dresden},
year = 2007,
topics = {team, lri},
month = apr,
type = {Diplomarbeit}
}
@mastersthesis{beauquier08master,
author = {Maxime Beauquier},
title = {Application du filtrage modulo associativit\'e et commutativit\'e ({AC}) \`a la r\'e\'ecriture de sous-termes modulo {AC} dans {Coq}},
school = {Master Parisien de Recherche en Informatique},
topics = {team},
type_publi = {rapport},
type_digiteo = {no},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@mastersthesis{bobot08master,
author = {Fran\c{c}ois Bobot},
title = {Satisfiabilit\'e de formules closes modulo une th\'eorie avec \'egalit\'e
et pr\'edicats},
school = {Master Parisien de Recherche en Informatique},
topics = {team},
type_publi = {rapport},
type_digiteo = {no},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@mastersthesis{gay08master,
author = {Steven Gay},
title = {Analyse d'\'echappement de port\'ee en {ReactiveML}},
school = {Master Parisien de Recherche en Informatique},
topics = {team},
type_publi = {rapport},
type_digiteo = {no},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@misc{cime3,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
title = {{CiME3}},
year = 2007,
url = {{http://cime.lri.fr}},
note = {\url{http://cime.lri.fr}},
topics = {team,lri},
type_publi = {autre},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@misc{coccinelle,
author = {\'Evelyne Contejean},
title = {{Coccinelle}},
year = 2005,
url = {{http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}},
note = {\url{http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}},
topics = {team,lri},
type_publi = {autre},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@misc{alt-ergo,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
title = {The {Alt-Ergo} Automated Theorem Prover},
note = {\url{http://alt-ergo.lri.fr/}},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL}
}
@misc{ergo,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {The {Alt-Ergo} automatic Theorem Prover},
url = {http://alt-ergo.lri.fr/},
howpublished = {\url{http://alt-ergo.lri.fr/}},
note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@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}
}
@mastersthesis{hubert04dea,
author = {Thierry Hubert},
title = {{Certification des preuves de terminaison en Coq}},
type = {Rapport de {DEA}},
year = 2004,
month = sep,
school = {Universit{\'e} Paris 7},
topics = {team, lri},
note = {\url{http://www.lri.fr/~marche/hubert04rr.ps}},
url = {http://www.lri.fr/~marche/hubert04rr.ps}
}
@manual{MandelMaranget2007Jocaml,
author = {Louis Mandel and Luc Maranget},
title = {The {JoCaml} system},
institution = {Inria-Rocquencourt},
note = {Software and documentation available at
\url{http://jocaml.inria.fr/}},
year = 2007,
url = {http://jocaml.inria.fr/},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion},
topics = {team}
}
@mastersthesis{sozeau05master,
author = {Matthieu Sozeau},
title = {{Coercion par pr{\'e}dicats en {Coq}}},
school = {Universit{\'e} Paris 7},
year = 2005,
note = {In French},
topics = {team},
type_publi = {rapport},
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport},
url = {http://mattam.org/research/publications/Coercion par prédicats en Coq.pdf}
}
@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}
}
@manual{lucy:manual06,
author = {Marc Pouzet},
title = {{Lucid Synchrone}, version 3.
Tutorial and reference manual},
organization = {Universit\'e Paris-Sud, LRI},
month = apr,
year = 2006,
topics = {team},
type_publi = {autre},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
url = {http://www.lri.fr/~pouzet/lucid-synchrone}
}
@mastersthesis{lescuyer06master,
author = {St\'ephane Lescuyer},
title = {Codage de la logique du premier ordre polymorphe multi-sort\'ee
dans la logique sans sortes},
school = {Master Parisien de Recherche en Informatique},
topics = {team},
type_publi = {rapport},
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport},
year = 2006
}
@manual{CoqManualV82,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version V8.2}},
year = 2008,
note = {\url{http://coq.inria.fr}},
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion}
}
@manual{CoqManualV83,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version V8.3}},
year = 2010,
note = {\url{http://coq.inria.fr}},
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion}
}
@manual{CoqManualV86,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version V8.6}},
year = 2016,
note = {\url{http://coq.inria.fr}},
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion}
}
@manual{CoqSetoidV82,
author = {Matthieu Sozeau},
note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}},
title = {User defined equalities and relations},
institution = {INRIA},
year = 2008,
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@manual{CoqProgramV82,
author = {Matthieu Sozeau},
note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}, \url{http://coq.inria.fr/}},
title = {Program},
url = {http://coq.inria.fr/},
year = 2008,
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@manual{CoqTypeClassesV82,
author = {Matthieu Sozeau},
title = {Type Classes},
note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}},
organization = {INRIA},
year = 2008,
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@manual{CoqManualV81,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version V8.1}},
year = 2006,
month = jul,
url = {http://coq.inria.fr},
note = {\url{http://coq.inria.fr}},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL EXT},
x-type = {manuel},
x-support = {diffusion}
}
@misc{boldo09diffusion,
author = {Sylvie Boldo},
title = {Demandez le programme!},
howpublished = {Interstices},
year = {2009},
month = feb,
topics = {team, lri},
url = {http://interstices.info/demandez-le-programme},
note = {\url{http://interstices.info/demandez-le-programme}},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {diffusion},
x-scientific-popularization = {yes}
}
@manual{moy08manual,
title = {Jessie Plugin Tutorial, \emph{Lithium} version},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA},
year = 2008,
note = {\url{http://www.frama-c.cea.fr/jessie.html}},
url = {http://www.frama-c.cea.fr/jessie.html},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://www.frama-c.cea.fr/jessie/main.pdf}
}
@manual{moy09manual,
title = {Jessie Plugin Tutorial, \emph{Beryllium} version},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA},
year = 2009,
note = {\url{http://www.frama-c.cea.fr/jessie.html}},
url = {http://www.frama-c.cea.fr/jessie.html},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://www.frama-c.cea.fr/jessie/main.pdf}
}
@manual{moy10manual,
title = {Jessie Plugin, Boron version},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA},
year = 2010,
note = {\url{http://frama-c.com/jessie/jessie-tutorial.pdf}},
url = {http://frama-c.com/jessie/jessie-tutorial.pdf},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://frama-c.com/jessie/jessie-tutorial.pdf}
}
@manual{moy11jessie,
title = {The Jessie plugin
for Deduction Verification in Frama-C --- Tutorial and Reference Manual},
author = {Yannick Moy and Claude March\'e},
organization = {INRIA \& LRI},
year = 2011,
note = {\url{http://krakatoa.lri.fr/}},
url = {http://krakatoa.lri.fr},
topics = {team,lri},
type_publi = {manuel},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion},
x-pdf = {http://krakatoa.lri.fr/jessie.pdf}
}
@misc{ayad09,
author = {Ali Ayad and Claude March\'e},
title = {Behavioral Properties of Floating-Point Programs},
howpublished = {Hisseo publications},
year = 2009,
note = {\url{http://hisseo.saclay.inria.fr/ayad09.pdf}},
url = {http://hisseo.saclay.inria.fr/ayad09.pdf},
topics = {team}
}
@mastersthesis{tafat09master,
author = {Asma Tafat},
title = {Invariants et raffinements en
pr\'esence de partage},
school = {Universit\'e Paris 6},
topics = {team},
year = 2009,
url = {http://www.lri.fr/~marche/tafat09master.pdf}
}
@unpublished{milchior09,
author = {Arthur Milchior},
title = {Algorithme de matching, modulo \'egalit\'e, incr\'emental, typ\'e et persistant},
institution = {\'Ecole Normale Sup\'erieure, Paris},
note = {Rapport de stage L3},
rawebnote = {Rapport de stage L3},
topics = {team},
year = 2009
}
@misc{marche09ws,
author = {Claude March\'e},
title = {The {Krakatoa} tool for Deductive Verification of {Java}
Programs},
howpublished = {Winter School on Object-Oriented Verification,
Viinistu, Estonia},
month = jan,
year = 2009,
url = {http://krakatoa.lri.fr/ws/},
x-pdf = {http://krakatoa.lri.fr/ws/notes.pdf},
note = {\url{http://krakatoa.lri.fr/ws/}},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {diffusion},
x-type = {invitation}
}
@misc{boldo10diffusion,
author = {Sylvie Boldo},
title = {C'est la faute \`a l'ordinateur!},
howpublished = {Interstices -- Id\'ee re\c{c}ue},
year = {2010},
month = feb,
topics = {team, lri},
note = {\url{http://interstices.info/idee-recue-informatique-18}},
web = {http://interstices.info/idee-recue-informatique-18},
hal = {http://hal.inria.fr/inria-00534848/fr/},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {diffusion},
x-scientific-popularization = {yes}
}
@misc{boldo10-webtv,
author = {Sylvie Boldo},
x-equipes = {demons PROVAL},
x-support = {video},
x-type = {vulgarisation},
topics = {team},
title = {L'informatique},
web = {http://www.universcience.tv/media/1340/l-informatique.html},
note = {Quiz 5-12, \url{http://www.universcience.tv/media/1340/l-informatique.html}},
hal = {http://hal.inria.fr/inria-00534852/fr/},
month = apr,
year = 2010,
howpublished = {Universcience web television},
x-scientific-popularization = {yes}
}
@mastersthesis{herms09master,
author = {Paolo Herms},
title = {Partial Type Inference with Higher-Order Types},
school = {Universit\`a di Pisa},
year = 2009,
topics = {team}
}
@proceedings{audebaud10scp,
title = {Science of Computer Programming. Special issue on the Mathematics of Program Construction (MPC 2008)},
year = 2011,
volume = 76,
number = 3,
issn = {0167-6423},
doi = {10.1016/j.scico.2010.05.005},
x-equipes = {demons PROVAL ext},
x-support = {livre},
x-type = {editorial},
topics = {team},
publisher = {Elsevier Science Publishers},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
url = {http://www.sciencedirect.com/science/article/B6V17-508CCPM-1/2/05b9e659a964af2a63a054fe26f63705},
editor = {Philippe Audebaud and Christine Paulin-Mohring}
}
@misc{boldo08diffusion-2,
author = {Sylvie Boldo and Thierry Vi\'eville},
title = {L'informatique, ce n'est pas pour les filles},
howpublished = {Interstices},
year = {2008},
topics = {team},
month = sep,
url = {http://interstices.info/idee-recue-informatique-5},
note = {\url{http://interstices.info/idee-recue-informatique-5}},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {diffusion},
x-scientific-popularization = {yes}
}
@misc{boldo10diffusion-2,
author = {Sylvie Boldo},
title = {Un algorithme de d\'ecoupe de g\^ateau},
howpublished = {Interstices},
year = {2010},
topics = {team},
month = jul,
url = {http://interstices.info/decoupe},
note = {\url{http://interstices.info/decoupe}},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {diffusion},
x-scientific-popularization = {yes}
}
@misc{boldopodcast08,
author = {Sylvie Boldo},
title = {Pourquoi mon ordinateur calcule-t-il faux?},
howpublished = {Interstices},
year = {2008},
month = apr,
topics = {team},
note = {Podcast, \url{http://interstices.info/a-propos-calcul-ordinateurs}},
url = {http://interstices.info/a-propos-calcul-ordinateurs},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {diffusion},
x-scientific-popularization = {yes}
}
@misc{BobotPaskevich2011,
author = {Fran\c{c}ois Bobot and Andrei Paskevich},
title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
year = 2011,
topics = {team},
note = {Preliminary report. \url{http://hal.inria.fr/inria-00591414/}}
}
@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/}}
}
@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}}
}
@mastersthesis{lelay11master,
author = {Catherine Lelay},
title = {\'Etude de la diff\'erentiabilit\'e et de l'int\'egrabilit\'e en {C}oq : Application \`a la formule de d'{A}lembert pour l'\'equation des ondes},
school = {Universit\'e Paris 7},
note = {\url{http://www.lri.fr/~lelay/Rapport.pdf}},
year = 2011,
topics = {team},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {master}
}
@misc{gasparcoq2011,
author = {Nuno Gaspar},
title = {Mechanized Semantics into Concurrent Program verification},
howpublished = {\url{http://www.lri.fr/~gaspar/rgcoq.html}},
topics = {team},
month = sep,
year = 2011,
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {master},
note = {A documented Coq library, work in progress}
}
@unpublished{lupinski12,
author = {Nicolas Lupinski and Joel Falcou and Christine Paulin-Mohring},
title = {S\'emantiques d'un langage de squelettes},
topics = {team},
year = {2012},
x-equipes = {demons PROVAL archi},
x-support = {rapport},
x-type = {article},
note = {\url{http://www.lri.fr/~paulin/Skel}},
rawebnote = {\url{http://www.lri.fr/~paulin/Skel}}
}
@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/}}
}
@mastersthesis{clochard13master,
topics = {team},
author = {Martin Clochard},
title = {Proving Programs with binders, automatically},
school = {Master Parisien de Recherche en Informatique},
year = 2013
}
@unpublished{dross13,
topics = {team},
hal = {http://hal.inria.fr/hal-00915931},
title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
abstract = {SMT solvers are efficient tools to decide the
satisfiability of ground formulas, including a
number of built-in theories such as congruence,
linear arithmetic, arrays, and bit-vectors. Adding a
theory to that list requires delving into the
implementation details of a given SMT solver, and is
done mainly by the developers of the solver
itself. For many useful theories, one can
alternatively provide a first-order
axiomatization. However, in the presence of
quantifiers, SMT solvers are incomplete and exhibit
unpredictable behavior. Consequently, this approach
can not provide us with a complete and terminating
treatment of the theory of interest. In this paper,
we propose a framework to solve this problem, based
on the notion of instantiation patterns, also known
as triggers. Triggers are annotations that suggest
instances which are more likely to be useful in
proof search. They are implemented in all SMT
solvers that handle first-order logic and are
included in the SMT-LIB format. In our framework,
the user provides a theory axiomatization with
triggers, along with a proof of completeness and
termination properties of this axiomatization, and
obtains a sound, complete, and terminating solver
for her theory in return. We describe and prove a
corresponding extension of the traditional Abstract
DPLL Modulo Theory framework. Implementing this
mechanism in a given SMT solver requires a one-time
development effort. We believe that this effort is
not greater than that of adding a single decision
procedure to the same SMT solver. We have
implemented the proposed extension in the Alt-Ergo
prover and we discuss some implementation details in
the paper. To show that our framework can handle
complex theories, we prove completeness and
termination of a feature-rich axiomatization of
doubly-linked lists. Our tests show that our
approach results in a better performance of the
solver on goals that stem from the verification of
programs manipulating doubly-linked lists.},
language = {Anglais},
affiliation = {TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , AdaCore SAS - AdaCore SAS},
year = 2013,
pdf = {http://hal.inria.fr/hal-00915931/PDF/dross-article.pdf},
note = {Submitted}
}
@mastersthesis{ndjanda14,
topics = {team},
author = {Mbiada Ndjanda, Jacques Charles},
title = {{FCLLVM}: un compilateur int\'egr\'e \`a l'environnement {Frama-C}},
school = {Universit\'e Paris-Diderot},
year = 2014,
note = {\url{https://www.lri.fr/~jmbiadan/public/cea_intership_v1.pdf}}
}
@misc{vieville:hal-01238442,
topics = {team},
title = {{ Structures : organisation, complexit\'e, dynamique des mot-cl\'es
au sens inattendu}},
author = {Vieville, Thierry and Boldo, Sylvie and Masseglia, Florent and
Bernhard, Pierre},
year = {2015},
month = apr,
hal = {https://hal.inria.fr/hal-01238442},
note = {Article de vulgarisation sur pixees.fr},
hal_id = {hal-01238442},
hal_version = {v1},
x-scientific-popularization = {yes}
}
@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}
}
@unpublished{galloiswong18calculemus,
topics = {team},
title = {{A Coq formalization of digital filters}},
author = {Gallois-Wong, Diane and Boldo, Sylvie and Hilaire, Thibault},
hal = {https://hal.inria.fr/hal-01728828},
booktitle = {{CICM 2018 - 11th Conference on Intelligent Computer Mathematics}},
address = {Hagenberg, Austria},
editor = {Florian Rabe and William M. Farmer and Grant O. Passmore and Abdou Youssef},
series = {Intelligent Computer Mathematics},
pages = {87--103},
year = {2018},
month = aug,
doi = {10.1007/978-3-319-96812-4\_8},
pdf = {https://hal.inria.fr/hal-01728828/file/CICM18.pdf}
}
@misc{faissole:hal-01485397,
topics = {team},
title = {Synthetic topology in homotopy type theory for probabilistic programming},
author = {Faissole, Florian and Spitters, Bas},
howpublished = {PPS 2017 - Workshop on probabilistic programming semantics },
year = 2017,
month = jan,
hal = {https://hal.inria.fr/hal-01485397},
note = {Poster}
}
@unpublished{jaloyan18,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-01936105},
note = {working paper \url{https://hal.inria.fr/hal-01936105}},
year = 2018,
month = nov
}
@unpublished{volkova18a,
topics = {team},
title = {Arithmetic approaches for rigorous design of reliable Fixed-Point {LTI} filters},
author = {Volkova, Anastasia and Hilaire, Thibault and Lauter, Christoph},
hal = {https://hal.archives-ouvertes.fr/hal-01918650},
note = {working paper or preprint},
year = 2018,
month = nov,
keywords = {Eigendecomposition ; Gershgorin circles ; Reliable Computations ; Floating-Point Arithmetic ; Digital Filters ; Interval Arithmetic ; Multiple Precision ; Fixed-Point Arithmetic ; Table Maker's Dilemma}
}
@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}
}
@unpublished{boldo19wp,
topics = {team},
title = {Emulating round-to-nearest-ties-to-zero ''augmented'' floating-point operations using round-to-nearest-ties-to-even arithmetic},
author = {Boldo, Sylvie and Lauter, Christoph Q. and Muller, Jean-Michel},
hal = {https://hal.archives-ouvertes.fr/hal-02137968},
note = {working paper or preprint},
year = 2019,
month = oct
}
@unpublished{steinberg19wp,
topics = {team},
title = {Quantitative continuity and computable analysis in {Coq}},
author = {Steinberg, Florian and Thery, Laurent and Thies, Holger},
hal = {https://hal.inria.fr/hal-02088293},
note = {working paper or preprint},
year = 2019,
month = apr,
pdf = {https://hal.inria.fr/hal-02088293/file/paper.pdf},
hal_id = {hal-02088293},
hal_version = {v1}
}
@misc{steinberg19mla,
topics = {team},
title = {Some formal proofs of isomorphy and discontinuity},
author = {Steinberg, Florian and Thies, Holger},
hal = {https://hal.inria.fr/hal-02019174},
howpublished = {Third Workshop on Mathematical Logic and its Applications},
year = 2019,
month = mar
}
@unpublished{boldo22,
topics = {team},
title = {A {Coq} Formalization of the {Bochner} integral},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Leclerc, Louise},
hal = {https://hal.inria.fr/hal-03516749},
note = {working paper or preprint},
year = 2022
}
@unpublished{moreau22,
topics = {team},
title = {Compilation formellement v{\'e}rifi{\'e}e d'un langage pour le calcul formel},
author = {Moreau, Josu{\'e}},
hal = {https://inria.hal.science/hal-03824148},
note = {working paper or preprint},
year = 2022
}
@proceedings{types04,
editor = {Jean-Christophe Filli\^atre and Christine Paulin-Mohring and Benjamin Werner},
title = {Types for Proofs and Programs, International Workshop, TYPES
2004, Jouy-en-Josas, France, December 15-18,2004, Selected Papers},
booktitle = {TYPES 2004},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3839},
year = {2005},
topics = {team,lri},
isbn = {3-540-31428-8},
x-equipes = {demons PROVAL EXT},
x-type = {edition},
x-support = {actes}
}
@proceedings{jfla17,
topics = {team},
hal = {https://hal.inria.fr/hal-01662072},
title = {Journ\'ees Francophones des Langages Applicatifs},
editor = {Boldo, Sylvie and Signoles, Julien},
year = 2017,
booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Gourette, 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{mpc08,
editor = {Philippe Audebaud and Christine Paulin-Mohring},
title = {Mathematics of Program Construction, MPC 2008},
booktitle = {Mathematics of Program Construction, MPC 2008},
publisher = {Springer},
address = {Marseille, France},
month = jul,
series = {Lecture Notes in Computer Science},
volume = {5133},
topics = {team,lri},
year = {2008},
x-equipes = {demons PROVAL EXT},
x-type = {edition},
url = {http://www.springerlink.com/content/978-3-540-70593-2},
x-support = {actes}
}
@proceedings{postfoveoos10,
editor = {Bernhard Beckert and Claude March\'e},
title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
publisher = {Springer},
topics = {team},
series = {Lecture Notes in Computer Science},
volume = 6528,
month = jan,
year = 2011,
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-type = {edition},
x-cle-support = {FOVEOOS},
x-pays = {DE}
}
@proceedings{vstte17,
topics = {team},
hal = {https://hal.inria.fr/hal-01670145},
title = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
booktitle = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
month = dec,
year = 2017,
address = {Heidelberg, Germany},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Andrei Paskevich and Thomas Wies},
series = {Lecture Notes in Computer Science},
number = 10712,
publisher = {Springer}
}
@proceedings{itp13,
hal_id = {hal-00908865},
url = {http://hal.inria.fr/hal-00908865},
topics = {team},
title = {{Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings.}},
editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
language = {Anglais},
affiliation = {CELTIQUE - INRIA - IRISA , TOCCATA - INRIA - Laboratoire de Recherche en Informatique - LRI},
publisher = {Springer},
pages = {500},
volume = {7998},
series = {Lecture Notes in Computer Science},
audience = {internationale },
doi = {10.1007/978-3-642-39634-2},
year = {2013}
}
@proceedings{nsv2017,
topics = {team},
title = {10th International Workshop on Numerical Software Verification},
booktitle = {10th International Workshop on Numerical Software Verification},
editor = {Abate, Alessandro and Boldo, Sylvie},
hal = {https://hal.inria.fr/hal-01662076},
publisher = {{Springer}},
year = 2017,
month = jul
}