complete-report.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc complete-report.cite -ob complete-report.bib -c 'topics : "team" and $type="techreport" 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}}
@techreport{conchon10rr,
  author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
  title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
  institution = {{LRI, Universit\'e Paris Sud}},
  year = 2010,
  type = {Research Report},
  number = 1538,
  month = dec,
  topics = {team, lri},
  type_publi = {interne},
  type_digiteo = {no},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {rapport},
  x-pdf = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
  url = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
  abstract = {http://www.lri.fr/~contejea/publis/rr1538/abstract.html}
}
@techreport{contejean04rr,
  author = {\'Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain},
  title = {Mechanically proving termination using polynomial interpretations},
  institution = {LRI},
  year = {2004},
  type = {Research Report},
  number = {1382},
  type_publi = {interne},
  topics = {team},
  url = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz}
}
@techreport{contejean07rr,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {Certification of automated termination proofs},
  institution = {CEDRIC},
  year = 2007,
  type = {Research Report},
  number = 1185,
  month = {May},
  topics = {team},
  type_digiteo = {no},
  type_publi = {interne},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {rapport}
}
@techreport{Filliatre06rr1,
  author = {Jean-Christophe Filli\^atre},
  title = {{Backtracking iterators}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = 1428,
  month = jan,
  year = 2006,
  url = {http://www.lri.fr/~filliatr/publis/enum-rr.ps.gz},
  topics = {team, lri},
  type_publi = {interne},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {rapport}
}
@techreport{MandelMaranget07RR,
  author = {Louis Mandel and Luc Maranget},
  title = {Programming in {JoCaml} -- extended version},
  institution = {INRIA},
  year = 2007,
  number = 6261,
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelMaranget-RR-2007.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelMaranget-RR-2007.pdf},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {rapport}
}
@techreport{Mandel2006Assert4322,
  key = {D432-2},
  author = {Louis Mandel},
  title = {Prototype of {AADL} simulation in {SCADE}},
  type = {{ASSERT} Deliverable 4.3.2-2},
  institution = {ASSERT Project},
  month = nov,
  year = 2006,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {contrat},
  x-support = {rapport}
}
@techreport{Mandel2006Assert4321,
  key = {D432-1},
  author = {Louis Mandel},
  title = {Report on modeling {GALS} in {SCADE}},
  type = {{ASSERT} Deliverable 4.3.2-1},
  institution = {ASSERT Project},
  month = feb,
  year = 2006,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {contrat},
  x-support = {rapport}
}
@techreport{moy07rr1,
  author = {Yannick Moy},
  title = {Checking {C} Pointer Programs for Memory Safety},
  institution = {INRIA},
  year = {2007},
  month = oct,
  type = {Research Report},
  number = {6334},
  x-pdf = {http://www.lri.fr/~moy/publis/moy07rr1.pdf},
  url = {http://www.lri.fr/~moy/publis/moy07rr1.pdf},
  type_digiteo = {no},
  type_publi = {rapport},
  topics = {team, lri},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {rapport}
}
@techreport{paulinrandom06,
  author = {Christine Paulin-Mohring},
  title = {A library for reasoning on randomized algorithms in {Coq}},
  institution = {Universit\'e Paris Sud},
  topics = {team},
  year = 2006,
  month = jan,
  type = {Description of a {Coq} contribution},
  x-pdf = {http://www.lri.fr/~paulin/ALEA/library.pdf},
  url = {http://www.lri.fr/~paulin/ALEA/library.pdf},
  note = {\url{http://www.lri.fr/~paulin/ALEA/library.pdf}},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@techreport{paulinrandom07,
  author = {Christine Paulin-Mohring},
  title = {A library for reasoning on randomized algorithms in {Coq} - Version 2},
  institution = {Universit\'e Paris Sud},
  topics = {team},
  year = 2007,
  month = dec,
  type = {Description of a {Coq} contribution},
  x-pdf = {http://www.lri.fr/~paulin/ALEA/library.pdf},
  url = {http://www.lri.fr/~paulin/ALEA/library.pdf},
  note = {\url{http://www.lri.fr/~paulin/ALEA/library.pdf}},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@techreport{signoles06semrfn,
  author = {Julien Signoles},
  title = {{Towards a ML extension with Refinement: a Semantic Issue}},
  year = 2006,
  month = mar,
  institution = {LRI, University of Paris Sud},
  number = 1440,
  url = {http://www.lri.fr/~signoles/publis/signoles06semrfn.pdf},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {rapport}
}
@techreport{chaudhary04demoney,
  author = {Vikrant Chaudhary},
  title = {The {Krakatoa} tool for certification of {Java/JavaCard} programs annotated in {JML} : A Case Study},
  institution = {IIT internship report},
  topics = {team,lri},
  year = 2004,
  month = jul
}
@techreport{lucas05tr,
  author = {Salvador Lucas and Claude March\'e and Jos\'e Meseguer},
  title = {Operational Termination of Conditional Term Rewriting Systems},
  institution = {Departamento de Sistemas Inform\'aticos y Computaci\'on},
  year = 2005,
  type = {Research Report},
  number = {DSIC II/01/05},
  address = {Universidad Polit\'ecnica de Valencia, Spain},
  month = feb,
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {rapport}
}
@techreport{couchot08report,
  author = {Jean-Fran\c{c}ois Couchot and Alain Giorgetti and Nicolas Stouls},
  title = {{Graph-based Reduction of Program Verification Conditions}},
  institution = {INRIA Saclay -- \^Ile-de-France},
  year = {2008},
  type = {Research Report},
  number = {6702},
  month = oct,
  hal = {http://hal.inria.fr/inria-00339847/en/},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {rapport}
}
@techreport{paskevich09rr,
  author = {Andrei Paskevich},
  title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
  institution = {INRIA},
  year = 2009,
  topics = {team},
  hal = {http://hal.inria.fr/inria-00439232/en/},
  note = {\url{http://hal.inria.fr/inria-00439232/en/}},
  number = 7128
}
@techreport{paskevich10rr,
  author = {Andrei Paskevich},
  title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform (version 2)},
  institution = {INRIA},
  year = 2010,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00439232/en/},
  note = {\url{http://hal.inria.fr/inria-00439232/en/}},
  number = 7128
}
@techreport{tushkanova09rr,
  title = {Modular Specification of {Java} Programs},
  author = {Tushkanova, Elena and Giorgetti, Alain and
            March{\'e}, Claude and Kouchnarenko, Olga},
  abstract = {This work investigates the question of modular
                  specification of generic {Java} classes and
                  methods. The first part introduces a specification
                  language for {Java} programs. In the second part the
                  language is used to specify an array sorting
                  algorithm by selection. The third and the fourth
                  parts define a syntax proposal for the specification
                  a generic {Java} programs, through two examples. The
                  former is the specification of the generic method
                  for sorting arrays which comes in the
                  \texttt{java.util.Arrays} class of the {Java}
                  {API}. The latter is the specification of the
                  \texttt{java.util.HashMap} class and its use for
                  memoization.},
  institution = {INRIA},
  number = 7097,
  year = 2009,
  topics = {team},
  hal = {http://hal.inria.fr/inria-00434452/en/}
}
@techreport{ayad09rr,
  title = {On formal methods for certifying floating-point {C} programs},
  author = {Ayad, Ali},
  type = {Research Report},
  institution = {INRIA},
  number = 6927,
  year = 2009,
  hal = {http://hal.inria.fr/inria-00383793/en/},
  topics = {team}
}
@techreport{tafat10rr,
  title = {A Refinement Approach for Correct-by-Construction Object-Oriented Programs},
  author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
  institution = {INRIA},
  number = 7310,
  year = 2010,
  x-equipes = {demons PROVAL EXT},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00491835/en/}
}
@techreport{bardou10rr,
  author = {Romain Bardou and Claude March\'e},
  title = {Regions and Permissions for Verifying Data Invariants},
  institution = {INRIA},
  year = 2010,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00525384/en/},
  note = {\url{http://hal.inria.fr/inria-00525384/en/}},
  type = {Research Report},
  number = 7412
}
@techreport{melquiond09cxx,
  author = {Guillaume Melquiond and Sylvain Pion},
  title = {Directed rounding arithmetic operations},
  institution = {ISO C++ Standardization Committee},
  number = {2899},
  year = {2009},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {rapport},
  topics = {team}
}
@techreport{contejean08rr,
  author = {\'Evelyne Contejean and Julien Forest and Xavier Urbain},
  title = {{Deep-Embedded Unification}},
  institution = {C\'edric laboratory, CNAM Paris, France},
  year = {2008},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  type = {Research Report},
  number = {1547},
  topics = {team}
}
@techreport{contejean11rr,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
                  and Olivier Pons and Xavier Urbain},
  title = {{Automated Certified Proofs with CiME3}},
  institution = {C\'edric laboratory, CNAM Paris, France},
  year = {2011},
  number = {2044},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  url = {http://cedric.cnam.fr/fichiers/art_2044.pdf},
  topics = {team},
  abstract = {http://www.lri.fr/~contejea/publis/rr2044/abstract.html}
}
@techreport{nguyen11rr,
  author = {Thi Minh Tuyen Nguyen and Claude March\'e},
  title = {Proving Floating-Point Numerical Programs by Analysis of
  their Assembly Code},
  institution = {INRIA},
  year = 2011,
  type = {Research Report},
  number = 7655,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00602266/en/},
  note = {\url{http://hal.inria.fr/inria-00602266/en/}}
}
@techreport{kalyan11rr,
  title = {Automated Generation of Loop Invariants using Predicate Abstraction},
  author = {Kalyanasundaram, K. and March{\'e}, Claude},
  type = {Research Report},
  institution = {INRIA},
  number = 7714,
  year = 2011,
  month = aug,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00615623/en/},
  note = {\url{http://hal.inria.fr/inria-00615623/en/}}
}
@techreport{tafat11rr,
  title = {Binary Heaps Formally Verified in {Why3}},
  author = {Tafat, Asma and March{\'e}, Claude},
  type = {Research Report},
  institution = {INRIA},
  number = 7780,
  year = 2011,
  month = oct,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00636083/en/},
  note = {\url{http://hal.inria.fr/inria-00636083/en/}}
}
@techreport{herms11rr,
  title = {A Certified Multi-prover Verification Condition Generator},
  author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
  x-equipes = {demons PROVAL ext},
  topics = {team},
  institution = {INRIA},
  year = 2011,
  x-support = {rapport},
  x-type = {article},
  hal = {http://hal.inria.fr/hal-00639977/en/},
  note = {\url{http://hal.inria.fr/hal-00639977/en/}},
  type = {Research Report},
  number = 7793
}
@techreport{MarMelMul11,
  hal = {http://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408/en/},
  title = {Some issues related to double roundings},
  author = {{\'E}rik Martin-Dorel and Guillaume Melquiond and Jean-Michel Muller},
  topics = {team},
  x-equipes = {demons PROVAL ext},
  x-support = {rapport},
  institution = {INRIA},
  year = {2011}
}
@techreport{BCFMMW11rr,
  hal_id = {hal-00649240},
  hal = {http://hal.inria.fr/hal-00649240/en/},
  note = {\url{http://hal.inria.fr/hal-00649240/en/}},
  title = {Wave Equation Numerical Resolution: Mathematics and Program},
  author = {Boldo, Sylvie and Cl\'ement, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
  abstract = {We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.},
  keywords = {Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis},
  language = {Anglais},
  affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI , ESTIME - INRIA Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rh{\^o}ne-Alpes / LIP Laboratoire de l'Informatique du Parall{\'e}lisme},
  pages = {30},
  type = {Research Report},
  institution = {INRIA},
  number = 7826,
  year = 2011,
  month = dec,
  pdf = {http://hal.inria.fr/hal-00649240/PDF/RR-7826.pdf},
  topics = {team},
  x-equipes = {demons PROVAL ext},
  x-support = {rapport}
}
@techreport{dross12rr,
  title = {Reasoning with Triggers},
  author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes
                  and Paskevich, Andrei},
  abstract = {SMT solvers can decide the satisfiability of ground
                  formulas modulo a combination of built-in
                  theories. Adding a built-in theory to a given SMT
                  solver is a complex and time consuming task that
                  requires internal knowledge of the solver. However,
                  many theories can be easily expressed using
                  first-order formulas. Unfortunately, since universal
                  quantifiers are not handled in a complete way by SMT
                  solvers, these axiomatics cannot be used as decision
                  procedures. In this paper, we show how to extend a
                  generic SMT solver to accept a custom theory
                  description and behave as a decision procedure for
                  that theory, provided that the described theory is
                  complete and terminating in a precise sense. The
                  description language consists of first-order axioms
                  with triggers, an instantiation mechanism that is
                  found in many SMT solvers. This mechanism, which
                  usually lacks a clear semantics in existing
                  languages and tools, is rigorously defined here;
                  this definition can be used to prove completeness
                  and termination of the theory. We demonstrate on two
                  examples, how such proofs can be achieved in our
                  formalism.},
  keywords = {Quantifiers, Triggers, SMT Solvers, Theories},
  language = {English},
  affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI},
  pages = 29,
  type = {Research Report},
  institution = {INRIA},
  number = {RR-7986},
  year = 2012,
  month = jun,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00703207},
  pdf = {http://hal.inria.fr/hal-00703207/PDF/RR-7986.pdf}
}