complete-journal.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc complete-journal.cite -ob complete-journal.bib -c 'topics : "team" and $type="article" and year>=2004' /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}}
@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 = {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 = {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}
}
@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{bol08tc3,
  author = {Sylvie Boldo},
  title = {{K}ahan's algorithm for a correct discriminant computation at last formally proven},
  journal = {IEEE Transactions on Computers},
  volume = {58},
  number = {2},
  issn = {0018-9340},
  year = {2009},
  pages = {220-225},
  doi = {10.1109/TC.2008.200},
  publisher = {IEEE Computer Society},
  month = feb,
  topics = {team,lri},
  type_publi = {irevcomlec},
  type_digiteo = {revue_cl},
  x-pdf = {http://hal.inria.fr/docs/00/17/14/97/PDF/discri.pdf},
  hal = {http://hal.inria.fr/inria-00171497/en/},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {ITComputers},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@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},
  hal = {http://hal.archives-ouvertes.fr/inria-00534350/fr/},
  doi = {10.1145/1644001.1644002}
}
@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},
  url = {http://proval.lri.fr/publications/boldo11mcs.pdf},
  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.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}
}
@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},
  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{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}
}