complete-journal.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc complete-journal.cite -ob complete-journal.bib -c 'topics : "team" and $type="article" and year>=2004' /users/demons/filliatr/bibliodemons/abbrevs.bib /users/demons/filliatr/bibliodemons/demons.bib /users/demons/filliatr/bibliodemons/demons2.bib /users/demons/filliatr/bibliodemons/demons3.bib /users/demons/filliatr/bibliodemons/team.bib /users/demons/filliatr/bibliodemons/crossrefs.bib}}
@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 = {http://dx.doi.org/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 = {http://dx.doi.org/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},
  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 = {http://doi.ieeecomputersociety.org/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 = {http://doi.ieeecomputersociety.org/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},
  x-pdf = {http://hal.inria.fr/docs/00/08/04/27/PDF/odd-rounding.pdf},
  hal = {http://hal.inria.fr/inria-00080427/en/},
  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},
  x-pdf = {http://hal.inria.fr/docs/00/33/75/37/PDF/RuZiBoMe08.pdf},
  hal = {http://hal.inria.fr/inria-00337537/en/},
  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},
  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},
  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 = {http://dx.doi.org/10.1007/s11786-011-0099-9},
  url = {http://proval.lri.fr/publications/boldo11mcs.pdf}
}
@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 = {2012},
  topics = {team},
  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},
  topics = {team},
  type_publi = {irevcomlec}
}
@article{boldo12jar,
  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 = {2012},
  optvolume = {},
  optnumber = {},
  optpages = {},
  optmonth = {},
  note = {Accepted for publication. \url{http://hal.inria.fr/hal-00649240/en/}},
  hal = {http://hal.inria.fr/hal-00649240/en/},
  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 = {},
  optmonth = {},
  note = {Accepted for publication.},
  topics = {team},
  type_publi = {irevcomlec}
}
@article{Benzaken13tods,
  author = {V. Benzaken and G. Castagna and D. Colazzo and K. Nguyen},
  title = {Optimizing {XML} querying using type-based document projection},
  journal = {ACM Transactions on Database Systems (TODS)},
  year = 2013,
  note = {To appear},
  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}
}