complete-report.bib

@comment{{This file has been generated by bib2bib 1.97pl3}}
@comment{{Command line: bib2bib -q -oc complete-report.cite -ob complete-report.bib -c 'topics : "team" and $type="techreport" and year>=2004' /users/demons/filliatr/toccata/web/biblio/bibliodemons/abbrevs.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/demons.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/demons2.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/demons3.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/team.bib /users/demons/filliatr/toccata/web/biblio/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},
  note = {\url{http://hal.inria.fr/inria-00439232}},
  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, Krishnamani 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},
  keywords = {Why3},
  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{BCFMMW11rr,
  hal_id = {hal-00649240},
  hal = {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,
  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,
  x-equipes = {demons PROVAL ext},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/hal-00703207},
  pdf = {http://hal.inria.fr/hal-00703207/PDF/RR-7986.pdf}
}
@techreport{blanchette12tr,
  author = {Jasmin C. Blanchette and Andrei Paskevich},
  title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
  institution = {Tech. Univ. Munich},
  year = 2012,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  url = {http://www21.in.tum.de/~blanchet/tff1spec.pdf},
  note = {\url{http://www21.in.tum.de/~blanchet/tff1spec.pdf}}
}
@techreport{marche12rr,
  title = {Weakest Precondition Calculus, revisited using {Why3}},
  author = {Claude March\'e and Asma Tafat},
  type = {Research Report},
  institution = {INRIA},
  number = {RR-8185},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  year = 2012,
  month = dec,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00766171},
  pdf = {http://hal.inria.fr/hal-00766171/PDF/RR-8185.pdf}
}
@techreport{rousseau13,
  hal = {http://hal.inria.fr/hal-00804915},
  topics = {team},
  hal_id = {hal-00804915},
  url = {http://hal.inria.fr/hal-00804915},
  title = {M{\'e}diation Scientifique : une facette de nos m{\'e}tiers de la recherche},
  author = {Rousseau, Antoine and Darnaud, Aur{\'e}lie and Goglin, Brice and Acharian, C{\'e}line and Leininger, Christine and Godin, Christophe and Holik, Clarisse and Kirchner, Claude and Rives, Diane and Darquie, Elodie and Kerrien, Erwan and Neyret, Fabrice and Masseglia, Florent and Dufour, Florian and Berry, G{\'e}rard and Dowek, Gilles and Robak, H{\'e}l{\`e}ne and Xypas, H{\'e}l{\`e}ne and Illina, Irina and Gnaedig, Isabelle and Jongwane, Joanna and Ehrel, Jocelyne and Viennot, Laurent and Guion, Laure and Calderan, Lisette and Kovacic, Lola and Collin, Marie and Enard, Marie-Agn{\`e}s and Comte, Marie-H{\'e}l{\`e}ne and Quinson, Martin and Olivi, Martine and Giraud, Mathieu and Dor{\'e}mus, Mathilde and Ogouchi, Mia and Droin, Muriel and Lacaux, Nathalie and Rougier, Nicolas and Roussel, Nicolas and Guitton, Pascal and Peterlongo, Pierre and Cornus, Rose-Marie and Vandermeersch, Simon and Maheo, Sophie and Lefebvre, Sylvain and Boldo, Sylvie and Vi{\'e}ville, Thierry and Poirel, V{\'e}ronique and Chabreuil, Aline and Fischer, Arnaud and Farge, Claude and Vadel, Claude and Astic, Isabelle and Dumont, Jean-Pierre and F{\'e}joz, Loic and Rambert, Patrick and Paradinas, Pierre and De Quatrebarbes, Sophie and Laurent, St{\'e}phane},
  abstract = {Dans ce monde devenu num{\'e}rique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du num{\'e}rique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen ma{\^\i}trise, au del{\`a} des usages, les principaux fondements de cette mutation num{\'e}rique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque coll{\`e}gue Inria int{\'e}ress{\'e} {\`a} participer {\`a} ce volet de nos missions. Devenue une facette de notre m{\'e}tier, comme le rappelle le Plan Strat{\'e}gique Inria [1], ce que nous appelons m{\'e}diation scientifique en sciences du num{\'e}rique (alias, " mecsci ") se professionnalise et change d'{\'e}chelle. Et c'est environ 1 \% de nos ressources qui a vocation {\`a} y {\^e}tre consacr{\'e}. Pour tout l'institut on parle donc de pr{\`e}s de 40 {\'e}quivalents temps-plein distribu{\'e}s {\`a} travers le travail quotidien ou ponctuel de plusieurs centaines de coll{\`e}gues chercheurs, ing{\'e}nieurs, communicants, etc.. Une telle {\'e}nergie m{\'e}rite d'{\^e}tre bien employ{\'e}e : au service des meilleurs objectifs ; vers des cibles bien d{\'e}finies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident {\`a} faire bouger les choses ; et avec une m{\'e}thodologie efficace qui optimise ce que nous investissons dans de telles activit{\'e}s ; tout en respectant et en encourageant les dynamiques locales et individuelles ind{\'e}pendantes qui restent les sources vives de la m{\'e}diation scientifique. Voil{\`a} pourquoi il y a juste besoin d'offrir en partage {\`a} chacune et chacun les {\'e}l{\'e}ments fondateurs et m{\'e}thodologiques de cette m{\'e}diation scientifique. Offrir aussi quelques bonnes pratiques tr{\`e}s concr{\`e}tes. On parle donc ici d'une organisation distribu{\'e}e d'actions collaboratives d'o{\`u} {\'e}merge le service public de popularisation scientifique vis{\'e}. C'est ce que ce document se propose de d{\'e}crire ici.},
  keywords = {m{\'e}diation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public.},
  language = {Fran{\c c}ais},
  affiliation = {MOISE - INRIA Grenoble Rh{\^o}ne-Alpes / LJK Laboratoire Jean Kuntzmann , INRIA Paris-Rocquencourt - INRIA , RUNTIME - INRIA Bordeaux - Sud-Ouest , Laboratoire Bordelais de Recherche en Informatique - LaBRI , INRIA Si{\`e}ge - INRIA , Virtual Plants - VP , UMR Am{\'e}lioration G{\'e}n{\'e}tique et Adaptation des Plantes M{\'e}diterran{\'e}eennes et Tropicales - AGAP , PAREO - INRIA Lorraine - LORIA , MAGRIT - INRIA Nancy - Grand Est / LORIA , MAVERICK - Inria Grenoble Rh{\^o}ne-Alpes / LJK Laboratoire Jean Kuntzmann , Laboratoire d'Informatique de Robotique et de Micro{\'e}lectronique de Montpellier - LIRMM , ZENITH - INRIA Sophia Antipolis , INRIA Sophia Antipolis - INRIA Sophia Antipolis , DEDUCTEAM - INRIA Paris-Rocquencourt , PAROLE - INRIA Nancy - Grand Est / LORIA , CARTE - INRIA Nancy - Grand Est / LORIA , GANG - INRIA Rocquencourt , Laboratoire d'informatique Algorithmique : Fondements et Applications - LIAFA , Laboratory of Information, Network and Communication Sciences - LINCS , Service IST Sophia Antipolis M{\'e}diterran{\'e}e / Laboratoire I3S - INRIA Sophia Antipolis - M{\'e}diterran{\'e}e , ALGORILLE - INRIA Nancy - Grand Est / LORIA , APICS - INRIA Sophia Antipolis , Laboratoire d'Informatique Fondamentale de Lille - LIFL , BONSAI - INRIA Lille - Nord Europe , FUSCIA - INRIA , CORTEX - INRIA Lorraine - LORIA , MINT - INRIA Lille - Nord Europe , GENSCALE - INRIA - IRISA , ALICE - INRIA Nancy - Grand Est / LORIA , Laboratoire de Recherche en Informatique - LRI , TOCCATA - INRIA Saclay - {\^I}le-de-France , Mnemosyne - INRIA Bordeaux - Sud-Ouest , MADYNES - INRIA Lorraine - LORIA , MOSEL - INRIA Lorraine - LORIA , Centre for Quantitative methods and Operations Management - QuantOM},
  pages = 34,
  type = {Interne},
  institution = {Inria},
  year = 2013,
  month = mar
}
@techreport{auger13rr1560,
  hal = {http://hal.archives-ouvertes.fr/hal-00834633},
  topics = {team},
  author = {C\'edric Auger and Zohir Bouzid and Pierre Courtieu and S\'ebastien Tixeuil and Xavier Urbain},
  title = {Certified Impossibility Results for Byzantine-Tolerant Mobile Robots},
  institution = {LRI},
  year = {2013},
  type = {Research Report},
  number = {1560},
  month = jun,
  pdf = {http://hal.archives-ouvertes.fr/docs/00/83/46/33/PDF/rr.pdf},
  url = {http://arxiv.org/abs/1306.4242}
}
@techreport{acar15rr,
  topics = {team},
  title = {Fast Parallel Graph-Search with Splittable and Catenable Frontiers},
  author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
  hal = {https://hal.inria.fr/hal-01089125},
  type = {Technical Report},
  institution = {Inria},
  year = 2015,
  month = jan
}
@techreport{dross15rr,
  topics = {team},
  title = {High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs},
  author = {Dross, Claire and Fumex, Cl{\'e}ment and Gerlach, Jens and March{\'e}, Claude},
  hal = {https://hal.inria.fr/hal-01238376},
  type = {Research Report},
  number = 8821,
  institution = {Inria},
  year = 2015,
  month = dec
}
@techreport{hauzar16rr,
  topics = {team},
  title = {Counterexamples from proof failures in the {SPARK} program verifier},
  author = {Hauzar, David and March{\'e}, Claude and Moy, Yannick},
  hal = {https://hal.inria.fr/hal-01271174},
  type = {Research Report},
  number = {RR-8854},
  institution = {Inria Saclay Ile-de-France},
  year = 2016,
  month = feb
}
@techreport{gondelman16reg,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {A Pragmatic Type System for Deductive Verification},
  type = {Research Report},
  institution = {Universit\'e Paris Sud},
  year = 2016,
  abstract = { In the context of deductive verication, it is customary
                  today to handle programs with pointers using either
                  separation logic, dynamic frames, or explicit memory
                  models. Yet we can observe that in numerous
                  programs, a large amount of code ts within the scope
                  of Hoare logic, provided we can statically control
                  aliasing. When this is the case, the code
                  correctness can be reduced to simpler verication
                  conditions which do not require any explicit memory
                  model. This makes verication conditions more
                  amenable both to automated theorem proving and to
                  manual inspection and debugging. In this paper, we
                  devise a method of such static aliasing control for
                  a programming language featuring nested data
                  structures with mutable components. Our solution is
                  based on a type system with singleton regions and
                  eects, which we prove to be sound.},
  hal = {https://hal.archives-ouvertes.fr/hal-01256434v3},
  note = {\url{https://hal.archives-ouvertes.fr/hal-01256434v3}}
}
@techreport{chen16rr,
  topics = {team},
  title = {A Formal Proof of a {Unix} Path Resolution Algorithm},
  author = {Ran Chen and Martin Clochard and Claude March\'e},
  hal = {https://hal.inria.fr/hal-01406848},
  type = {Research Report},
  number = {RR-8987},
  institution = {Inria},
  year = 2016,
  month = dec
}
@techreport{fumex17rr,
  topics = {team},
  title = {Automated Verification of Floating-Point Computations in {Ada}
           Programs},
  author = {Fumex, Cl{\'e}ment and March{\'e}, Claude and Moy, Yannick},
  hal = {https://hal.inria.fr/hal-01511183},
  type = {Research Report},
  number = {RR-9060},
  pages = 53,
  institution = {Inria},
  year = 2017,
  month = apr
}
@techreport{dami17,
  topics = {team},
  title = {The {CoLiS} language: syntax, semantics and associated tools},
  author = {Dami, Ilham and March{\'e}, Claude},
  hal = {https://hal.inria.fr/hal-01614488},
  type = {Technical Report},
  number = 0491,
  institution = {Inria},
  year = 2017,
  month = oct
}
@techreport{baudin17,
  topics = {team},
  title = {Deductive Verification with the Help of Abstract Interpretation},
  author = {Lucas Baudin},
  hal = {https://hal.inria.fr/hal-01634318},
  type = {Technical Report},
  institution = {Univ Paris-Sud},
  year = 2017,
  month = nov
}
@techreport{clochard18rr,
  topics = {team},
  title = {Deductive Verification via Ghost Debugging},
  author = {Clochard, Martin and Paskevich, Andrei and March{\'e}, Claude},
  hal = {https://hal.inria.fr/hal-01907894},
  type = {Research Report},
  number = 9219,
  institution = {Inria},
  year = 2018
}
@techreport{jeannerod19tr,
  topics = {team},
  title = {Specification of {UNIX} Utilities},
  author = {Jeannerod, Nicolas and R{\'e}gis-Gianas, Yann and March{\'e}, Claude and Sighireanu, Mihaela and Treinen, Ralf},
  hal = {https://hal.inria.fr/hal-02321691},
  type = {Technical Report},
  institution = {HAL Archives Ouvertes},
  year = 2019,
  month = oct
}
@techreport{becker19tr,
  topics = {team},
  title = {Revision 2 of {CoLiS} language: formal syntax, semantics, concrete and symbolic interpreters},
  author = {Becker, Benedikt and March{\'e}, Claude and Jeannerod, Nicolas and Treinen, Ralf},
  hal = {https://hal.inria.fr/hal-02321743},
  type = {Technical Report},
  institution = {HAL Archives Ouvertes},
  year = 2019,
  month = oct
}
@techreport{huisman19rr,
  topics = {team},
  title = {VerifyThis 2018: A Program Verification Competition},
  author = {Huisman, Marieke and Monahan, Rosemary and M{\"u}ller, Peter and Paskevich, Andrei and Ernst, Gidon},
  hal = {https://hal.inria.fr/hal-01981937},
  type = {Research Report},
  institution = {Universit{\'e} Paris-Saclay},
  year = 2019,
  month = jan
}
@techreport{andres19rr,
  topics = {team},
  title = {V\'erification par preuve formelle de propri\'et\'es fonctionnelles d'algorithme de classification},
  author = {Andr\`es, L\'eo},
  hal = {https://hal.inria.fr/hal-02421484},
  type = {Rapport de stage de {M1}},
  institution = {Universit\'e Paris Sud},
  year = 2019,
  month = aug
}
@techreport{becker20rr,
  topics = {team},
  title = {Rapport d'avancement sur la v{\'e}rification formelle des algorithmes de {ParcourSup}},
  author = {Becker, Benedikt and Filli{\^a}tre, Jean-Christophe and March{\'e}, Claude},
  hal = {https://hal.inria.fr/hal-02447409},
  type = {Technical Report},
  institution = {Universit{\'e} Paris-Saclay},
  year = 2020,
  month = jan
}