doc/manual.bib

   1 @comment{{This file has been generated by bib2bib 1.98}}
   2
   3 @comment{{Command line: bib2bib -c '$key="ergo" or $key="dailler18jlamp" or $key="ieee754-2008" or $key="barrett11cade" or $key="okasaki98" or $key="CoqArt" or $key="paskevich09rr" or $key="vstte10comp" or $key="hauzar16sefm" or $key="conchon08smt" or $key="filliatre07cav" or 1=2' /home/cmarche/biblio/abbrevs.bib /home/cmarche/biblio/demons.bib /home/cmarche/biblio/demons2.bib /home/cmarche/biblio/demons3.bib /home/cmarche/biblio/team.bib /home/cmarche/biblio/crossrefs.bib}}
   4
   5 @string{sv = {Springer}}
   6
   7 @string{lncs = {Lecture Notes in Computer Science}}
   8
   9 @techreport{baudin17,
  10   topics = {team},
  11   TITLE = {Deductive Verification with the Help of Abstract Interpretation},
  12   AUTHOR = {Lucas Baudin},
  13   hal = {https://hal.inria.fr/hal-01634318},
  14   TYPE = {Technical Report},
  15   INSTITUTION = {Univ Paris-Sud},
  16   YEAR = 2017,
  17   MONTH = nov
  18 }
  19
  20 @book{CoqArt,
  21   author = {Yves Bertot and Pierre Castéran},
  22   title = {Interactive Theorem Proving and Program Development},
  23   subtitle = {Coq'Art: The Calculus of Inductive Constructions},
  24   publisher = {Springer-Verlag},
  25   series = {Texts in Theoretical Computer Science},
  26   year = 2004,
  27   doi = {10.1007/978-3-662-07964-5}
  28 }
  29
  30 @misc{ieee754-2008,
  31   key = {IEEE754},
  32   abstract = {This standard specifies interchange and arithmetic
  33                   formats and methods for binary and decimal
  34                   floating-point arithmetic in computer programming
  35                   environments. This standard specifies exception
  36                   conditions and their default handling. An
  37                   implementation of a floating-point system conforming
  38                   to this standard may be realized entirely in
  39                   software, entirely in hardware, or in any
  40                   combination of software and hardware. For operations
  41                   specified in the normative part of this standard,
  42                   numerical results and exceptions are uniquely
  43                   determined by the values of the input data, sequence
  44                   of operations, and destination formats, all under
  45                   user control.},
  46   booktitle = {{IEEE} Std 754-2008},
  47   doi = {10.1109/IEEESTD.2008.4610935},
  48   journal = {IEEE Std 754-2008},
  49   pages = {1--58},
  50   title = {{IEEE} Standard for Floating-Point Arithmetic},
  51   year = {2008},
  52 }
  53
  54 @misc{vstte10comp,
  55   author = {Natarajan Shankar and Peter Mueller},
  56   title = {{Verified Software: Theories, Tools and Experiments
  57                   (VSTTE'10). Software Verification Competition}},
  58   month = {August},
  59   year = 2010,
  60   address = {Edinburgh, Scotland},
  61   url = {http://www.macs.hw.ac.uk/vstte10/Competition.html}
  62 }
  63
  64 @book{okasaki98,
  65   author = {Chris Okasaki},
  66   title = {Purely Functional Data Structures},
  67   publisher = {Cambridge University Press},
  68   year = 1998
  69 }
  70
  71 @inproceedings{barrett11cade,
  72   author = {Barrett, Clark and Conway, Christopher L. and Deters, Morgan and Hadarean, Liana and Jovanović, Dejan and King, Tim and Reynolds, Andrew and Tinelli, Cesare},
  73   title = {{CVC4}},
  74   booktitle = {23rd International Conference on Computer Aided Verification},
  75   year = 2011,
  76   isbn = {978-3-642-22109-5},
  77   address = {Snowbird, UT},
  78   pages = {171--177},
  79   numpages = 7,
  80   url = {http://dl.acm.org/citation.cfm?id=2032305.2032319},
  81   acmid = 2032319,
  82   publisher = {Springer-Verlag},
  83 }
  84
  85 @inproceedings{conchon08smt,
  86   author = {François Bobot and Sylvain Conchon and Évelyne Contejean
  87   and Stéphane Lescuyer},
  88   title = {{Implementing Polymorphism in SMT solvers}},
  89   booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
  90   pages = {1--5},
  91   year = 2008,
  92   editor = {Clark Barrett and Leonardo de Moura},
  93   volume = 367,
  94   series = {ACM International Conference Proceedings Series},
  95   topics = {team,lri},
  96   type_digiteo = {conf_autre},
  97   type_publi = {colloque},
  98   x-equipes = {demons PROVAL},
  99   x-type = {article},
 100   x-support = {actes_aux},
 101   x-cle-support = {SMT},
 102   x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
 103   url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
 104   x-editorial-board = {yes},
 105   x-international-audience = {yes},
 106   x-proceedings = {yes},
 107   isbn = {978-1-60558-440-9},
 108   doi = {10.1145/1512464.1512466},
 109   abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
 110 }
 111
 112 @misc{ergo,
 113   author = {Sylvain Conchon and Évelyne Contejean},
 114   title = {The {Alt-Ergo} automatic Theorem Prover},
 115   url = {http://alt-ergo.lri.fr/},
 116   topics = {team,lri},
 117   year = 2008,
 118   x-equipes = {demons PROVAL},
 119   x-type = {manuel},
 120   x-support = {diffusion}
 121 }
 122
 123 @inproceedings{filliatre07cav,
 124   author = {Jean-Christophe Filliâtre and Claude Marché},
 125   title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
 126   Verification},
 127   booktitle = {19th International Conference on Computer Aided Verification},
 128   editor = {Werner Damm and Holger Hermanns},
 129   series = lncs,
 130   volume = 4590,
 131   address = {Berlin, Germany},
 132   month = jul,
 133   year = {2007},
 134   pages = {173--177},
 135   topics = {team, lri},
 136   url = {https://hal.inria.fr/inria-00270820v1},
 137   type_digiteo = {conf_isbn},
 138   type_publi = {icolcomlec},
 139   x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
 140   x-equipes = {demons PROVAL EXT},
 141   x-type = {articlecourt},
 142   x-support = {actes},
 143   x-cle-support = {CAV},
 144   doi = {10.1007/978-3-540-73368-3_21}
 145 }
 146
 147 @techreport{paskevich09rr,
 148   author = {Andrei Paskevich},
 149   title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
 150   institution = {INRIA},
 151   year = 2009,
 152   topics = {team},
 153   url = {http://hal.inria.fr/inria-00439232},
 154   number = 7128
 155 }
 156
 157 @inproceedings{hauzar16sefm,
 158   topics = {team},
 159   author = {Hauzar, David and Marché, Claude and Moy, Yannick},
 160   title = {Counterexamples from Proof Failures in {SPARK}},
 161   booktitle = {Software Engineering and Formal Methods},
 162   year = 2016,
 163   pages = {215--233},
 164   doi = {10.1007/978-3-319-41591-8_15},
 165   editor = {De Nicola, Rocco and Eva Kühn},
 166   series = lncs,
 167   address = {Vienna, Austria},
 168   url = {https://hal.inria.fr/hal-01314885}
 169 }
 170
 171 @article{dailler18jlamp,
 172   topics = {team},
 173   title = {Instrumenting a Weakest Precondition Calculus for Counterexample Generation},
 174   author = {Dailler, Sylvain and Hauzar, David and Marché, Claude and Moy, Yannick},
 175   url = {https://hal.inria.fr/hal-01802488},
 176   journal = {Journal of Logical and Algebraic Methods in Programming},
 177   publisher = {Elsevier},
 178   volume = 99,
 179   pages = {97--113},
 180   year = 2018,
 181   keywords = {Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples}
 182 }
 183
 184
 185 @Manual{baudin18acsl,
 186   title =        {{ACSL}: {ANSI/ISO C} Specification Language},
 187   author =       {Patrick Baudin  and Jean-Christophe Filliâtre and Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
 188   year =         2018,
 189   note =         {\url{https://frama-c.com/acsl.html}},
 190   url =          {https://frama-c.com/acsl.html},
 191   x-pdf =        {https://frama-c.com/download/acsl_1.14.pdf}
 192 }
 193
 194 @inproceedings{filliatre07mix,
 195   author = {Jean-Christophe Filli\^atre},
 196   title = {{Formal Verification of MIX Programs}},
 197   booktitle = {{Journ{\'e}es en l'honneur de Donald E. Knuth}},
 198   year = 2007,
 199   note = {\url{http://knuth07.labri.fr/exposes.php}},
 200   address = {Bordeaux, France},
 201   month = {October},
 202   url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf}
 203 }
 204
 205
 206
 207 @phdthesis{nguyen12phd,
 208   author = {Nguyen, Thi Minh Tuyen},
 209   title = {Taking architecture and compiler into account
 210 in formal proofs of numerical programs},
 211   school = {Universit{\'e} Paris-Sud},
 212   type = {Th{\`e}se de Doctorat},
 213   url = {http://tel.archives-ouvertes.fr/tel-00710193},
 214   year = 2012,
 215   month = jun
 216 }
 217
 218 @inproceedings{paskevich20isola,
 219   author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
 220   title = {Abstraction and Genericity in Why3},
 221   booktitle = {9th International Symposium On Leveraging Applications of Formal
 222                   Methods, Verification and Validation (ISoLA)},
 223   month = oct,
 224   year = 2020,
 225   publisher = {Springer},
 226   series = {Lecture Notes in Computer Science},
 227   volume = 12476,
 228   pages = {122--142},
 229   editor = {Tiziana Margaria and Bernhard Steffen},
 230   address = {Rhodes, Greece},
 231   topics = {team},
 232   url = {http://why3.lri.fr/isola-2020/},
 233   hal = {https://hal.inria.fr/hal-02696246}
 234 }