complete-journal.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc complete-journal.cite -ob complete-journal.bib -c 'topics : "team" and $type="article" and year>=2004' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@article{boldo14jar,
author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
title = {{Verified Compilation of Floating-Point Computations}},
journal = {Journal of Automated Reasoning},
volume = {54},
number = {2},
pages = {135-163},
year = {2015},
month = feb,
publisher = {{Springer Verlag (Germany)}},
hal = {https://hal.inria.fr/hal-00862689},
topics = {team,lri},
type_publi = {irevcomlec}
}
@article{boldo14larecherche,
hal = {http://hal.inria.fr/ensl-01069744},
author = {Sylvie Boldo and Jean-Michel Muller},
title = {Des ordinateurs capables de calculer plus juste},
journal = {La Recherche},
year = {2014},
volume = {492},
pages = {46--52},
month = oct,
topics = {team,lri},
type_publi = {diffusion}
}
@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}
}
@article{BLM14mcs,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Coquelicot: A User-Friendly Library of Real Analysis for {C}oq},
hal = {http://hal.inria.fr/hal-00860648},
journal = {Mathematics in Computer Science},
topics = {team},
issn = {1661-8270},
doi = {10.1007/s11786-014-0181-1},
month = jun,
year = {2015},
volume = {9},
number = {1},
publisher = {Springer Basel},
pages = {41-62}
}
@article{BLM14mscs,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
year = {2016},
hal = {http://hal.inria.fr/hal-00806920},
journal = {Mathematical Structures in Computer Science},
topics = {team}
}
@article{benzaken13tods,
author = {V\'eronique Benzaken and Giuseppe Castagna and Dario Colazzo and Kim Nguyen},
title = {Optimizing {XML} querying using type-based document projection},
journal = {ACM Transactions on Database Systems (TODS)},
year = 2013,
hal = {http://hal.archives-ouvertes.fr/hal-00798049},
topics = {team,lri},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {TODS},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@article{benzaken08jacm,
author = {Alain Frisch and Giuseppe Castagna and V\'eronique Benzaken},
title = {Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types},
journal = {Journal of the ACM},
volume = {55},
number = {4},
year = {2008},
issn = {0004-5411},
pages = {1--64},
doi = {10.1145/1391289.1391293},
publisher = {ACM Press},
address = {New York, NY, USA},
topics = {team,lri},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {JACM},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@article{conchon12lmcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {Canonized Rewriting and Ground {AC} Completion Modulo {Shostak} Theories : Design and Implementation},
journal = {Logical Methods in Computer Science},
year = {2012},
month = sep,
pages = {1--29},
volume = 8,
number = 3,
hal = {http://hal.inria.fr/hal-00798082},
url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-international-audience = {yes},
x-editorial-board = {yes},
x-cle-support = {LMCS},
doi = {10.2168/LMCS-8(3:16)2012},
note = {Selected Papers of the Conference \emph{Tools and Algorithms for the Construction and Analysis of Systems} (TACAS 2011), Saarbr{\"u}cken, Germany, 2011}
}
@article{audebaud07scp,
author = {Philippe Audebaud and Christine Paulin-Mohring},
title = {Proofs of Randomized Algorithms in {Coq}},
journal = {Science of Computer Programming},
year = 2009,
volume = {74},
number = {8},
pages = {568--589},
topics = {team},
type_publi = {irevcomlec},
type_digiteo = {revue_cl},
doi = {10.1016/j.scico.2007.09.002},
x-pdf = {http://www.lri.fr/~paulin/ALEA/random-scp.pdf},
hal = {http://hal.inria.fr/inria-00431771/en/},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {SCP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@article{conchon06tcs,
author = {Sylvain Conchon and Sava Krsti{\'c}},
title = {Strategies for Combining Decision Procedures},
journal = {Theoretical Computer Science},
year = 2006,
volume = 354,
number = 2,
pages = {187--210},
note = {Special Issue of TCS dedicated to a refereed
selection of papers presented at TACAS'03},
topics = {team,lri},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {TCS}
}
@article{krstic-conchon-05,
author = {Sava Krsti{\'c} and Sylvain Conchon},
title = {Canonization for disjoint unions of theories},
journal = {Information and Computation},
volume = {199},
month = {May},
year = {2005},
pages = {87--106},
topics = {team},
number = {1-2},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {JIC}
}
@article{contejean05jar,
author = {\'Evelyne Contejean and Claude March{\'e} and Ana Paula Tom{\'a}s and Xavier Urbain},
title = {Mechanically proving termination using polynomial
interpretations},
journal = {Journal of Automated Reasoning},
volume = {34},
number = {4},
pages = {325--363},
year = 2005,
type_publi = {irevcomlec},
topics = {team},
doi = {10.1007/s10817-005-9022-x},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {JAR},
abstract = {http://www.lri.fr/~contejea/publis/2005jar/abstract.html}
}
@article{duran06hosc,
author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier Urbain},
title = {Proving Operational Termination of Membership Equational Programs},
journal = {Higher-Order and Symbolic Computation},
year = 2008,
type_publi = {irevcomlec},
type_digiteo = {revue_cl},
topics = {team},
volume = 21,
number = {1--2},
pages = {59--88},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-editorial-board = {yes},
x-international-audience = {yes},
x-cle-support = {HSC},
x-pdf = {http://www.lri.fr/~marche/duran08hosc.pdf},
hal = {http://hal.inria.fr/inria-00431474/en/},
url = {http://www.lri.fr/~marche/duran08hosc.pdf}
}
@article{Filliatre99c,
author = {Jean-Christophe Filli\^atre},
title = {{Formal Proof of a Program: Find}},
journal = {Science of Computer Programming},
year = 2006,
volume = 64,
pages = {332--240},
doi = {10.1016/j.scico.2006.10.002},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/find.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/find.pdf},
topics = {team, lri},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-cle-support = {SCP}
}
@article{marche2004jsc,
author = {Claude March\'e and Xavier Urbain},
title = {Modular and Incremental Proofs of {AC}-Termination},
journal = {Journal of Symbolic Computation},
volume = 38,
pages = {873--897},
year = 2004,
topics = {team},
type_digiteo = {revue_cl},
type_publi = {irevcomlec},
url = {http://authors.elsevier.com/sd/article/S074771710400029X}
}
@article{MandelPouzet2007TSI,
author = {Louis Mandel and Marc Pouzet},
title = {{ReactiveML} : un langage fonctionnel pour la programmation r{\'e}active},
journal = {Technique et Science Informatiques ({TSI})},
year = {2008},
volume = 27,
number = {9--10/2008},
pages = {1097--1128},
x-pdf = {http://www.lri.fr/~mandel/papers/MandelPouzet-TSI-2007.pdf},
url = {http://www.lri.fr/~mandel/papers/MandelPouzet-TSI-2007.pdf},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-cle-support = {TSI},
x-editorial-board = {yes},
x-international-audience = {no}
}
@article{marche04jlap,
author = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
title = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
journal = {Journal of Logic and Algebraic Programming},
year = 2004,
volume = 58,
number = {1--2},
pages = {89--106},
note = {\url{http://krakatoa.lri.fr}},
url = {http://krakatoa.lri.fr},
ps = {http://www.lri.fr/~marche/marche04jlap.ps},
topics = {team},
type_publi = {irevcomlec}
}
@article{urbain04jar,
author = {Xavier Urbain},
title = {Modular and Incremental Automated Termination Proofs},
journal = {Journal of Automated Reasoning},
year = {2004},
volume = 32,
pages = {315--355},
topics = {team},
type_publi = {irevcomlec},
url = {http://www.lri.fr/~urbain/textes/jar.ps.gz}
}
@article{bol08tc2,
author = {Sylvie Boldo and Marc Daumas and Ren-Cang Li},
title = {Formally Verified Argument Reduction with a Fused-Multiply-Add},
journal = {IEEE Transactions on Computers},
year = {2009},
volume = {58},
number = {8},
issn = {0018-9340},
pages = {1139-1145},
doi = {10.1109/TC.2008.216},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
url = {http://arxiv.org/abs/0708.3722},
topics = {team,lri},
type_publi = {irevcomlec},
type_digiteo = {revue_cl},
x-pdf = {http://arxiv.org/pdf/0708.3722v1},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {ITComputers},
x-editorial-board = {yes},
x-international-audience = {yes},
x-pays = {US}
}
@article{bol08tc1,
author = {Sylvie Boldo and Guillaume Melquiond},
title = {Emulation of {FMA} and {C}orrectly-{R}ounded {S}ums: {P}roved {A}lgorithms {U}sing {R}ounding to {O}dd},
journal = {IEEE Transactions on Computers},
year = {2008},
volume = {57},
number = {4},
pages = {462--471},
topics = {team,lri},
type_digiteo = {revue_cl},
type_publi = {irevcomlec},
hal = {http://hal.inria.fr/inria-00080427/},
doi = {10.1109/TC.2007.70819},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {ITComputers},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@article{girault06tecs,
author = {Alain Girault and Xavier Nicollin and Marc Pouzet},
title = {{Automatic Rate Desynchronization of Embedded Reactive
Programs}},
journal = {ACM Transactions on Embedded Computing Systems (TECS)},
volume = 5,
number = 3,
topics = {team},
year = 2006,
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {TECS}
}
@article{lucas05ipl,
topics = {team},
author = {Salvador Lucas and Claude March\'e and Jos\'e Meseguer},
title = {Operational Termination of Conditional Term Rewriting Systems},
journal = {Information Processing Letters},
publisher = {Elsevier North-Holland, Inc.},
volume = 95,
pages = {446--453},
year = 2005,
type_publi = {irevcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {IPL},
x-international-audience = {yes},
x-language = {en},
abstract = {We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs}
}
@article{lucy:jdaes10,
author = {Marc Pouzet and Pascal Raymond},
title = {{Modular Static Scheduling of Synchronous Data-flow
Networks: An efficient symbolic representation}},
journal = {Journal of Design Automation for Embedded Systems},
year = 2010,
note = {Special issue of selected papers from
\url{http://esweek09.inrialpes.fr/}{Embedded System Week}},
x-equipes = {demons PROVAL EXT},
x-support = {revue},
x-cle-support = {JDAES},
x-type = {article},
topics = {team}
}
@article{bolmel09bit,
author = {Siegfried M. Rump and Paul Zimmermann and Sylvie Boldo and Guillaume Melquiond},
title = {Computing predecessor and successor in rounding to nearest},
journal = {BIT},
year = {2009},
volume = {49},
number = {2},
month = jun,
pages = {419--431},
doi = {10.1007/s10543-009-0218-z},
hal = {http://hal.inria.fr/inria-00337537/},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-pays = {DE},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@article{daumas09toms,
author = {Marc Daumas and Guillaume Melquiond},
title = {Certification of bounds on expressions involving rounded operators},
journal = {Transactions on Mathematical Software},
publisher = {ACM Press},
year = {2010},
volume = {37},
number = {1},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {TOMS},
x-international-audience = {yes},
x-editorial-board = {yes},
type_publi = {irevcomlec},
pages = {1--20},
doi = {10.1145/1644001.1644003},
hal = {hal-00127769}
}
@article{boldo10-tc,
title = {Exact and {A}pproximated error of the {FMA}},
author = {Boldo, Sylvie and Muller, Jean-Michel},
abstract = {The fused multiply accumulate-add (FMA) instruction,
specified by the IEEE 754-2008 Standard for
Floating-Point Arithmetic, eases some calculations,
and is already available on some current processors
such as the Power PC or the Itanium. We first extend
an earlier work on the computation of the exact
error of an FMA (by giving more general conditions
and providing a formal proof). Then, we present a
new algorithm that computes an approximation to the
error of an FMA, and provide error bounds and a
formal proof for that algorithm.},
journal = {IEEE Transactions on Computers},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
year = {2011},
month = feb,
volume = {60},
number = {2},
pages = {157--164},
hal = {http://hal.inria.fr/inria-00429617/en/},
topics = {team},
x-equipes = {demons PROVAL},
x-international-audience = {yes},
x-editorial-board = {yes},
x-support = {diffusion},
x-type = {article}
}
@article{moy10jsc,
author = {Yannick Moy and Claude March\'e},
title = {Modular Inference of Subprogram Contracts for Safety Checking},
journal = {Journal of Symbolic Computation},
year = 2010,
volume = 45,
hal = {http://hal.inria.fr/inria-00534331/en/},
doi = {10.1016/j.jsc.2010.06.004},
x-international-audience = {yes},
x-editorial-board = {yes},
pages = {1184-1211},
x-equipes = {demons PROVAL ext},
x-support = {revue},
x-cle-support = {JSC},
x-type = {article},
topics = {team}
}
@article{dinechin10tc,
hal = {http://hal.inria.fr/inria-00533968/en/},
title = {Certifying the floating-point implementation of an elementary function using {G}appa},
author = {de Dinechin, Florent and Lauter, Christoph and Melquiond, Guillaume},
publisher = {{IEEE} Comp. Soc. Press},
journal = {{IEEE} {T}ransactions on {C}omputers },
pages = {242--253},
volume = {60},
number = {2},
x-equipes = {demons PROVAL ext},
x-international-audience = {yes},
x-editorial-board = {yes},
x-pays = {US},
topics = {team},
doi = {10.1109/TC.2010.128},
year = 2011
}
@article{boldo11-isse,
author = {Sylvie Boldo and Thi Minh Tuyen Nguyen},
title = {Proofs of numerical programs when the compiler optimizes},
journal = {Innovations in Systems and Software Engineering},
year = {2011},
pages = {151--160},
volume = {7},
issue = {2},
hal = {http://hal.inria.fr/hal-00777639},
x-international-audience = {yes},
x-editorial-board = {yes},
topics = {team},
x-support = {revue},
x-equipes = {demons PROVAL},
x-type = {article},
x-cle-support = {ISSE}
}
@article{boldo11mcs,
author = {Sylvie Boldo and Claude March\'e},
title = {Formal verification of numerical programs: from {C} annotated programs to mechanical proofs},
journal = {Mathematics in Computer Science},
topics = {team},
x-type = {article},
x-support = {revue},
x-cle-support = {MCS},
x-equipes = {demons PROVAL},
x-international-audience = {yes},
x-editorial-board = {yes},
year = 2011,
publisher = {Birkhauser Basel},
issn = {1661-8270},
pages = {377--393},
volume = {5},
issue = {4},
doi = {10.1007/s11786-011-0099-9},
hal = {http://hal.inria.fr/hal-00777605}
}
@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}
}
@article{MelNowZim12,
hal = {http://hal.inria.fr/hal-00644166/en/},
title = {Numerical Approximation of the {M}asser-{G}ramain Constant to Four Decimal Digits: delta=1.819\ldots},
author = {Guillaume Melquiond and Werner Georg Nowak and Paul Zimmermann},
publisher = {AMS},
journal = {Mathematics of Computation},
year = {2013},
volume = {82},
pages = {1235--1246},
doi = {10.1090/S0025-5718-2012-02635-4},
topics = {team},
x-type = {article},
x-support = {revue},
x-cle-support = {MoC},
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL ext},
type_publi = {irevcomlec}
}
@article{melquiond12,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
journal = {Information and Computation},
volume = {216},
pages = {14--23},
year = {2012},
doi = {10.1016/j.ic.2011.09.005},
hal = {http://hal.inria.fr/hal-00797913},
topics = {team},
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL},
x-support = {revue},
x-cle-support = {JIC},
x-type = {article},
type_publi = {irevcomlec}
}
@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}
}
@article{nguyen13spe,
author = {Arroyuelo, Diego and Claude, Francisco and Maneth, Sebastian and M\"{a}kinen, Veli and Navarro, Gonzalo and Nguyen, Kim and Sir\'en, Jouni and V\"{a}lim\"{a}ki, Niko},
title = {Fast in-memory {XP}ath search using compressed indexes},
journal = {Software: Practice and Experience},
issn = {1097-024X},
doi = {10.1002/spe.2227},
pages = {n/a--n/a},
keywords = {XML, succinct data structures, XPath, tree automata},
year = {2013},
type_publi = {irevcomlec},
topics = {team}
}
@article{martindorel13bit,
hal = {http://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408},
topics = {team},
title = {Some Issues related to Double Roundings},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume and Muller, Jean-Michel},
volume = {53},
number = {4},
pages = {897--924},
journal = {BIT Numerical Mathematics},
audience = {internationale},
doi = {10.1007/s10543-013-0436-2},
year = 2013
}
@article{dross16jar,
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-01221066},
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.},
year = 2016,
journal = {Journal of Automated Reasoning},
volume = 56,
number = 4,
pages = {387--457}
}
@article{bobot14sttt,
topics = {team},
doi = {10.1007/s10009-014-0314-5},
hal_id = {hal-00967132},
hal = {http://hal.inria.fr/hal-00967132/en},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Let's Verify This with {Why3}},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
volume = 17,
number = 6,
pages = {709--727},
year = 2015,
note = {See also \url{http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html}},
publisher = {Springer Berlin / Heidelberg},
x-type = {article},
x-support = {revue},
x-cle-support = {STTT},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@article{marche14scp,
topics = {team},
doi = {10.1016/j.scico.2014.04.003},
hal_id = {hal-00967124},
hal = {http://hal.inria.fr/hal-00967124/en},
title = {Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study},
author = {March{\'e}, Claude},
abstract = {We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving},
publisher = {Elsevier},
journal = {Science of Computer Programming},
year = 2014,
volume = 96,
number = 3,
pages = {279--296},
month = mar,
pdf = {http://hal.inria.fr/hal-00967124/PDF/main.pdf}
}
@article{gondelman16fmsd,
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
journal = {Formal Methods in System Design},
publisher = {Springer},
year = 2016,
volume = 48,
number = 3,
pages = {152--174},
issn = {1572-8102},
doi = {10.1007/s10703-016-0243-x},
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-01396864v1},
keywords = {Why3},
type_publi = {irevcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {revue},
x-editorial-board = {yes},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.
}
}
@article{martindorel14jar,
topics = {team},
hal = {http://hal.inria.fr/hal-00919498},
year = 2014,
journal = {Journal of Automated Reasoning},
doi = {10.1007/s10817-014-9312-2},
title = {Formally Verified Certificate Checkers for Hardest-to-Round Computation},
publisher = {Springer Netherlands},
keywords = {Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic},
author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
pages = {1--29},
language = {English}
}
@article{marche15ercim,
topics = {team},
hal = {http://hal.inria.fr/hal-01102242},
author = {Claude March\'e and Johannes Kanig},
title = {Bridging the Gap between Testing and Formal
Verification in {Ada} Development},
journal = {ERCIM News},
year = 2015,
volume = 100,
pages = {38--39},
month = jan
}
@article{filliatre14tangente,
author = {Jean-Christophe Filli\^atre},
title = {D\'emonstration. L'ordinateur \`a la rescousse},
journal = {Tangente (hors-s\'erie num\'ero 52)},
year = 2014,
number = 52,
pages = {34--36},
month = {February},
topics = {team,lri},
type_publi = {diffusion}
}
@article{martindorel15jara,
topics = {team},
title = {Proving Tight Bounds on Univariate Expressions with Elementary Functions in {Coq}},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01086460},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2016,
doi = {10.1007/s10817-015-9350-4},
keywords = {Coq proof assistant ; formal proof ; decision procedure ; interval arithmetic ; floating-point arithmetic ; nonlinear arithmetic}
}
@article{roux15jar,
topics = {team},
title = {Formal Proofs of Rounding Error Bounds},
author = {Roux, Pierre},
hal = {https://hal.archives-ouvertes.fr/hal-01091189},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2015,
doi = {10.1007/s10817-015-9339-z},
keywords = {floating-point arithmetic ; rounding error ; numerical analysis ; proof assistant ; Coq ; matrices ; Cholesky decomposition}
}
@article{martindorel15jarb,
topics = {team},
title = {Formally verified certificate checkers for hardest-to-round computation},
author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
hal = {https://hal.inria.fr/hal-00919498},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 54,
number = 1,
pages = {1-29},
year = 2015,
doi = {10.1007/s10817-014-9312-2},
keywords = {formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic}
}
@article{boldo17toms,
topics = {team},
title = {On the robustness of the {2Sum} and {Fast2Sum} algorithms},
author = {Boldo, Sylvie and Graillat, Stef and Muller, Jean-Michel},
hal = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023},
journal = {ACM Transactions on Mathematical Software},
publisher = {ACM Press},
year = {2017},
volume = {44},
number = {1},
month = jul,
pdf = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023/file/FaithfulTwoSum-Final-Fev2017.pdf}
}
@article{clochard17jar,
topics = {team},
title = {The {Matrix} Reproved},
author = {Clochard, Martin and Gondelman, L{\'e}on and Pereira, M{\'a}rio},
hal = {https://hal.inria.fr/hal-01617437},
journal = {Journal of Automated Reasoning},
pages = {365--383},
volume = 60,
number = 3,
publisher = {Springer},
year = 2018,
doi = {10.1007/s10817-017-9436-2}
}
@article{acar:hal-01409069,
topics = {team},
title = {Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages},
author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike},
hal = {https://hal.inria.fr/hal-01409069},
journal = {Journal of Functional Programming},
publisher = {Cambridge University Press},
volume = 26,
year = 2016,
month = nov,
doi = {10.1017/S0956796816000101}
}
@article{chen17jfr,
topics = {team},
title = {A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links},
author = {Chen, Ran and Clochard, Martin and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01652148},
journal = {Journal of Formalized Reasoning},
volume = 10,
number = 1,
year = 2017,
pages = {51--66},
doi = {10.6092/issn.1972-5787/6767},
url = {https://jfr.unibo.it/article/view/6767}
}
@article{mahboubi19jar,
topics = {team},
title = {Formally Verified Approximations of Definite Integrals},
author = {Mahboubi, Assia and Melquiond, Guillaume and Sibut-Pinote, Thomas},
hal = {https://hal.inria.fr/hal-01630143},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 62,
number = 2,
pages = {281--300},
year = 2019,
month = feb,
doi = {10.1007/s10817-018-9463-7}
}
@article{dailler18jlamp,
topics = {team},
title = {Instrumenting a Weakest Precondition Calculus for Counterexample Generation},
author = {Dailler, Sylvain and Hauzar, David and March{\'e}, Claude and Moy, Yannick},
hal = {https://hal.inria.fr/hal-01802488},
journal = {Journal of Logical and Algebraic Methods in Programming},
publisher = {Elsevier},
volume = 99,
pages = {97--113},
year = 2018,
doi = {10.1016/j.jlamp.2018.05.003},
keywords = {Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples}
}
@article{volkova18toc,
topics = {team},
title = {Towards Hardware {IIR} Filters Computing Just Right: Direct Form {I} Case Study},
author = {Volkova, Anastasia and Istoan, Matei and de Dinechin, Florent and Hilaire, Thibault},
hal = {https://hal.sorbonne-universite.fr/hal-01561052},
journal = {IEEE Transactions on Computers},
publisher = {Institute of Electrical and Electronics Engineers},
year = 2018,
keywords = {computer arithmetic ; fixed-point ; FPGA ; error analysis ; digital filters ; constant multiplication}
}
@article{galloiswong19na,
topics = {team},
title = {Optimal Inverse Projection of Floating-Point Addition},
author = {Gallois-Wong, Diane and Boldo, Sylvie and Cuoq, Pascal},
hal = {https://hal.inria.fr/hal-01939097},
journal = {Numerical Algorithms},
publisher = {Springer},
year = 2019,
doi = {10.1007/s11075-019-00711-z},
pdf = {https://hal.inria.fr/hal-01939097/file/main.pdf}
}
@article{boldo19toc,
topics = {team},
title = {Round-off error and exceptional behavior analysis of explicit {Runge-Kutta} methods},
author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
hal = {https://hal.archives-ouvertes.fr/hal-01883843},
journal = {IEEE Transactions on Computers},
publisher = {Institute of Electrical and Electronics Engineers},
year = 2019,
doi = {10.1109/TC.2019.2917902},
pdf = {https://hal.archives-ouvertes.fr/hal-01883843/file/article_hal.pdf}
}
@article{neumann19tcs,
topics = {team},
title = {Parametrised second-order complexity theory with applications to the study of interval computation},
author = {Neumann, Eike and Steinberg, Florian},
hal = {https://hal.inria.fr/hal-02148494},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
year = 2019,
doi = {10.1016/j.tcs.2019.05.009}
}
@article{filliatre20jlamp,
author = {Jean-Christophe Filli\^atre},
title = {Simpler Proofs with Decentralized Invariants},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = 121,
publisher = {Elsevier},
year = 2021,
topics = {team},
month = jan,
note = {See \url{https://usr.lmf.cnrs.fr/~jcf/spdi/}},
hal = {https://hal.inria.fr/hal-02518570},
doi = {https://doi.org/10.1016/j.jlamp.2021.100645}
}
@article{conchon20jar,
topics = {team},
title = {Parameterized Model Checking on the {TSO} Weak Memory Model},
author = {Conchon, Sylvain and Declerck, David and Za{\"i}di, Fatiha},
hal = {https://hal.inria.fr/hal-03149332},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 64,
number = 7,
pages = {1307--1330},
year = 2020
}
@article{galloiswong20na,
topics = {team},
title = {Optimal Inverse Projection of Floating-Point Addition},
author = {Gallois-Wong, Diane and Boldo, Sylvie and Cuoq, Pascal},
hal = {https://hal.inria.fr/hal-01939097},
journal = {Numerical Algorithms},
publisher = {Springer},
volume = 83,
number = 3,
pages = {957--986},
year = 2020,
doi = {10.1007/s11075-019-00711-z}
}
@article{boldo20tc,
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},
journal = {Transactions on Computers},
publisher = {{IEEE} Comp. Soc. Press},
year = 2020,
doi = {10.1109/TC.2020.3002702},
keywords = {Numerical reproducibility ; Floating-point arithmetic ; Numerical repro- ducibility ; Formal proof ; Rounding mode ; Error-free transforms ; Rounding error analysis}
}
@article{boldo21toc,
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},
journal = {IEEE Transactions on Computers},
volume = 70,
number = 7,
pages = {1046--1058},
year = 2021,
doi = {10.1109/TC.2020.3002702}
}
@article{steinberg21lmcs,
topics = {team},
title = {Computable analysis and notions of continuity in {Coq}},
author = {Steinberg, Florian and Th{\'e}ry, Laurent and Thies, Holger},
hal = {https://hal.inria.fr/hal-03324295},
journal = {Logical Methods in Computer Science},
doi = {10.23638/LMCS-17(2:16)2021},
year = 2021
}
@article{bensalemknapp22tetc,
topics = {team},
title = {Bounding the Round-Off Error of the Upwind Scheme for Advection},
author = {Ben Salem-Knapp, Louise and Boldo, Sylvie and Weens, William},
hal = {https://hal.inria.fr/hal-03329933},
journal = {IEEE Transactions on Emerging Topics in Computing},
publisher = {IEEE},
volume = 10,
number = 3,
year = 2022,
doi = {10.1109/TETC.2022.3191472},
keywords = {Round-off error ; Floating-Point ; Numerical Scheme ; Advection ; Hydrodynamics}
}
@article{belo22sttt,
topics = {team},
title = {Automated Formal Analysis of Temporal Properties of {Ladder} Programs},
author = {Belo Louren{\c c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03737869},
journal = {International Journal on Software Tools for Technology Transfer},
publisher = {Springer},
year = 2022,
pages = {977--997},
volume = 24,
number = 6,
doi = {10.1007/s10009-022-00680-0},
keywords = {Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment}
}
@article{becker22sttt,
topics = {team},
title = {The {CoLiS} Platform for the Analysis of Maintainer Scripts in {Debian} Software Packages},
author = {Becker, Benedikt and Jeannerod, Nicolas and March{\'e}, Claude and R{\'e}gis-Gianas, Yann and Sighireanu, Mihaela and Treinen, Ralf},
hal = {https://hal.inria.fr/hal-03737886},
journal = {International Journal on Software Tools for Technology Transfer},
publisher = {Springer},
year = 2022
}
@article{boldo22jar,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-03471095},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 66,
pages = {175--213},
year = 2022,
doi = {10.1007/s10817-021-09612-0}
}
@article{melquiond23jsc,
topics = {team},
title = {{WhyMP}, a Formally Verified Arbitrary-Precision Integer Library},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-03233220},
journal = {Journal of Symbolic Computation},
publisher = {Elsevier},
volume = 115,
pages = {74--95},
year = 2023,
doi = {10.1016/j.jsc.2022.07.007}
}
@article{rieuhelft19jfr,
topics = {team},
title = {A {Why3} proof of {GMP} algorithms},
author = {Rieu-Helft, Rapha{\"e}l},
hal = {https://inria.hal.science/hal-02477578},
journal = {Journal of Formalized Reasoning},
publisher = {ASDD-AlmaDL},
year = 2019,
doi = {10.6092/issn.1972-5787/9730}
}
@article{georges23jacm,
topics = {team},
title = {Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code},
author = {Georges, A{\"i}na Linn and Gu{\'e}neau, Arma{\"e}l and Van Strydonck, Thomas and Timany, Amin and Trieu, Alix and Devriese, Dominique and Birkedal, Lars},
hal = {https://hal.science/hal-03826854},
journal = {Journal of the ACM},
year = 2023,
doi = {10.1145/3623510}
}
@article{boldo23an,
topics = {team},
title = {Floating-point arithmetic},
author = {Boldo, Sylvie and Jeannerod, Claude-Pierre and Melquiond, Guillaume and Muller, Jean-Michel},
hal = {https://hal.science/hal-04095151},
journal = {Acta Numerica},
publisher = {Cambridge University Press},
volume = 32,
pages = {203--290},
year = 2023,
doi = {10.1017/S0962492922000101}
}
@article{conchon21fi,
topics = {team},
author = {Sylvain Conchon and Giorgio Delzanno and Angelo Ferrando},
title = {Declarative Parameterized Verification of Distributed Protocols via
the Cubicle Model Checker},
journal = {Fundam. Informaticae},
volume = 178,
number = 4,
pages = {347--378},
year = 2021,
doi = {10.3233/FI-2021-2010}
}
@article{martindorel23jar,
topics = {team},
title = {Enabling Floating-Point Arithmetic in the {Coq} Proof Assistant},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume and Roux, Pierre},
hal = {https://inria.hal.science/hal-04114233},
journal = {Journal of Automated Reasoning},
publisher = {Springer Verlag},
volume = 67,
number = 33,
year = 2023,
doi = {10.1007/s10817-023-09679-x}
}
@article{balabonski23lmcs,
topics = {team},
title = {{A strong call-by-need calculus}},
author = {Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
hal = {https://inria.hal.science/hal-03409681},
journal = {{Logical Methods in Computer Science}},
volume = 19,
number = 1,
year = 2023,
doi = {10.46298/lmcs-19(1:21)2023}
}