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 @string{eptcs = "Electronic Proceedings in Theoretical Computer Science"}
  10
  11 @techreport{baudin17,
  12   topics = {team},
  13   TITLE = {Deductive Verification with the Help of Abstract Interpretation},
  14   AUTHOR = {Lucas Baudin},
  15   url = {https://hal.inria.fr/hal-01634318},
  16   TYPE = {Technical Report},
  17   INSTITUTION = {Univ Paris-Sud},
  18   YEAR = 2017,
  19   MONTH = nov
  20 }
  21
  22 @book{CoqArt,
  23   author = {Yves Bertot and Pierre Castéran},
  24   title = {Interactive Theorem Proving and Program Development},
  25   subtitle = {Coq'Art: The Calculus of Inductive Constructions},
  26   publisher = {Springer-Verlag},
  27   series = {Texts in Theoretical Computer Science},
  28   year = 2004,
  29   doi = {10.1007/978-3-662-07964-5}
  30 }
  31
  32 @misc{ieee754-2008,
  33   key = {IEEE754},
  34   abstract = {This standard specifies interchange and arithmetic
  35                   formats and methods for binary and decimal
  36                   floating-point arithmetic in computer programming
  37                   environments. This standard specifies exception
  38                   conditions and their default handling. An
  39                   implementation of a floating-point system conforming
  40                   to this standard may be realized entirely in
  41                   software, entirely in hardware, or in any
  42                   combination of software and hardware. For operations
  43                   specified in the normative part of this standard,
  44                   numerical results and exceptions are uniquely
  45                   determined by the values of the input data, sequence
  46                   of operations, and destination formats, all under
  47                   user control.},
  48   booktitle = {{IEEE} Std 754-2008},
  49   doi = {10.1109/IEEESTD.2008.4610935},
  50   journal = {IEEE Std 754-2008},
  51   pages = {1--58},
  52   title = {{IEEE} Standard for Floating-Point Arithmetic},
  53   year = {2008},
  54 }
  55
  56 @misc{vstte10comp,
  57   author = {Natarajan Shankar and Peter Mueller},
  58   title = {{Verified Software: Theories, Tools and Experiments
  59                   (VSTTE'10). Software Verification Competition}},
  60   month = {August},
  61   year = 2010,
  62   address = {Edinburgh, Scotland},
  63   url = {http://www.macs.hw.ac.uk/vstte10/Competition.html}
  64 }
  65
  66 @book{okasaki98,
  67   author = {Chris Okasaki},
  68   title = {Purely Functional Data Structures},
  69   publisher = {Cambridge University Press},
  70   year = 1998
  71 }
  72
  73 @inproceedings{barrett11cade,
  74   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},
  75   title = {{CVC4}},
  76   booktitle = {23rd International Conference on Computer Aided Verification},
  77   year = 2011,
  78   isbn = {978-3-642-22109-5},
  79   address = {Snowbird, UT},
  80   pages = {171--177},
  81   numpages = 7,
  82   url = {http://dl.acm.org/citation.cfm?id=2032305.2032319},
  83   acmid = 2032319,
  84   publisher = {Springer-Verlag},
  85 }
  86
  87 @inproceedings{conchon08smt,
  88   author = {François Bobot and Sylvain Conchon and Évelyne Contejean
  89   and Stéphane Lescuyer},
  90   title = {{Implementing Polymorphism in SMT solvers}},
  91   booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
  92   pages = {1--5},
  93   year = 2008,
  94   editor = {Clark Barrett and Leonardo de Moura},
  95   volume = 367,
  96   series = {ACM International Conference Proceedings Series},
  97   topics = {team,lri},
  98   type_digiteo = {conf_autre},
  99   type_publi = {colloque},
 100   x-equipes = {demons PROVAL},
 101   x-type = {article},
 102   x-support = {actes_aux},
 103   x-cle-support = {SMT},
 104   x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
 105   url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
 106   x-editorial-board = {yes},
 107   x-international-audience = {yes},
 108   x-proceedings = {yes},
 109   isbn = {978-1-60558-440-9},
 110   doi = {10.1145/1512464.1512466},
 111   abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
 112 }
 113
 114 @misc{ergo,
 115   author = {Sylvain Conchon and Évelyne Contejean},
 116   title = {The {Alt-Ergo} automatic Theorem Prover},
 117   url = {http://alt-ergo.lri.fr/},
 118   topics = {team,lri},
 119   year = 2008,
 120   x-equipes = {demons PROVAL},
 121   x-type = {manuel},
 122   x-support = {diffusion}
 123 }
 124
 125 @inproceedings{filliatre07cav,
 126   author = {Jean-Christophe Filliâtre and Claude Marché},
 127   title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
 128   Verification},
 129   booktitle = {19th International Conference on Computer Aided Verification},
 130   editor = {Werner Damm and Holger Hermanns},
 131   series = lncs,
 132   volume = 4590,
 133   address = {Berlin, Germany},
 134   month = jul,
 135   year = {2007},
 136   pages = {173--177},
 137   topics = {team, lri},
 138   url = {https://hal.inria.fr/inria-00270820v1},
 139   type_digiteo = {conf_isbn},
 140   type_publi = {icolcomlec},
 141   x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
 142   x-equipes = {demons PROVAL EXT},
 143   x-type = {articlecourt},
 144   x-support = {actes},
 145   x-cle-support = {CAV},
 146   doi = {10.1007/978-3-540-73368-3_21}
 147 }
 148
 149 @techreport{paskevich09rr,
 150   author = {Andrei Paskevich},
 151   title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
 152   institution = {INRIA},
 153   year = 2009,
 154   topics = {team},
 155   url = {http://hal.inria.fr/inria-00439232},
 156   number = 7128
 157 }
 158
 159 @inproceedings{hauzar16sefm,
 160   topics = {team},
 161   author = {Hauzar, David and Marché, Claude and Moy, Yannick},
 162   title = {Counterexamples from Proof Failures in {SPARK}},
 163   booktitle = {Software Engineering and Formal Methods},
 164   year = 2016,
 165   pages = {215--233},
 166   doi = {10.1007/978-3-319-41591-8_15},
 167   editor = {De Nicola, Rocco and Eva Kühn},
 168   series = lncs,
 169   address = {Vienna, Austria},
 170   url = {https://hal.inria.fr/hal-01314885}
 171 }
 172
 173 @article{dailler18jlamp,
 174   topics = {team},
 175   title = {Instrumenting a Weakest Precondition Calculus for Counterexample Generation},
 176   author = {Dailler, Sylvain and Hauzar, David and Marché, Claude and Moy, Yannick},
 177   url = {https://hal.inria.fr/hal-01802488},
 178   journal = {Journal of Logical and Algebraic Methods in Programming},
 179   publisher = {Elsevier},
 180   volume = 99,
 181   pages = {97--113},
 182   year = 2018,
 183   keywords = {Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples}
 184 }
 185
 186
 187 @Manual{baudin18acsl,
 188   title =        {{ACSL}: {ANSI/ISO C} Specification Language},
 189   author =       {Patrick Baudin  and Jean-Christophe Filliâtre and Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
 190   year =         2018,
 191   url =          {https://frama-c.com/acsl.html},
 192   x-pdf =        {https://frama-c.com/download/acsl_1.14.pdf}
 193 }
 194
 195 @inproceedings{filliatre07mix,
 196   author = {Jean-Christophe Filliâtre},
 197   title = {{Formal Verification of MIX Programs}},
 198   booktitle = {{Journ{\'e}es en l'honneur de Donald E. Knuth}},
 199   year = 2007,
 200   note = {\url{http://knuth07.labri.fr/exposes.php}},
 201   address = {Bordeaux, France},
 202   month = {October},
 203   url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf}
 204 }
 205
 206
 207
 208 @phdthesis{nguyen12phd,
 209   author = {Nguyen, Thi Minh Tuyen},
 210   title = {Taking architecture and compiler into account
 211 in formal proofs of numerical programs},
 212   school = {Universit{\'e} Paris-Sud},
 213   type = {Th{\`e}se de Doctorat},
 214   url = {http://tel.archives-ouvertes.fr/tel-00710193},
 215   year = 2012,
 216   month = jun
 217 }
 218
 219 @inproceedings{paskevich20isola,
 220   author = {Jean-Christophe Filliâtre and Andrei Paskevich},
 221   title = {Abstraction and Genericity in {W}hy3},
 222   booktitle = {9th International Symposium On Leveraging Applications of Formal
 223                   Methods, Verification and Validation (ISoLA)},
 224   month = oct,
 225   year = 2020,
 226   publisher = {Springer},
 227   series = {Lecture Notes in Computer Science},
 228   volume = 12476,
 229   pages = {122--142},
 230   editor = {Tiziana Margaria and Bernhard Steffen},
 231   address = {Rhodes, Greece},
 232   topics = {team},
 233   note = "See also \url{http://why3.lri.fr/isola-2020/}",
 234   url = {https://hal.inria.fr/hal-02696246}
 235 }
 236
 237 @inproceedings{becker21fide,
 238   topics={team},
 239   TITLE = {Explaining Counterexamples with Giant-Step Assertion Checking},
 240   AUTHOR = {Becker, Benedikt and Belo Lourenço, Cláudio and Marché, Claude},
 241   URL = {https://hal.inria.fr/hal-03217393},
 242   BOOKTITLE = {6th Workshop on Formal Integrated Development Environments (F-IDE 2021)},
 243   EDITOR = {Creissac Campos, Jos{\'e} and Paskevich, Andrei},
 244   series = eptcs,
 245   doi = {10.4204/EPTCS.338.10},
 246   YEAR = 2021,
 247   MONTH = may
 248 }
 249
 250 @TechReport{gondelman16reg,
 251   topics = {team},
 252   author =       {Jean-Christophe Filliâtre and Léon Gondelman and Andrei Paskevich},
 253   title =        {A Pragmatic Type System for Deductive Verification},
 254   type = {Research report},
 255   institution =  {Universit\'e Paris Sud},
 256   year =         2016,
 257   abstract = { In the context of deductive verication, it is customary
 258                   today to handle programs with pointers using either
 259                   separation logic, dynamic frames, or explicit memory
 260                   models. Yet we can observe that in numerous
 261                   programs, a large amount of code ts within the scope
 262                   of Hoare logic, provided we can statically control
 263                   aliasing. When this is the case, the code
 264                   correctness can be reduced to simpler verication
 265                   conditions which do not require any explicit memory
 266                   model. This makes verication conditions more
 267                   amenable both to automated theorem proving and to
 268                   manual inspection and debugging. In this paper, we
 269                   devise a method of such static aliasing control for
 270                   a programming language featuring nested data
 271                   structures with mutable components. Our solution is
 272                   based on a type system with singleton regions and
 273                   eects, which we prove to be sound.},
 274   url = {https://hal.archives-ouvertes.fr/hal-01256434v3}
 275 }
 276
 277
 278 @INPROCEEDINGS{flanagan01popl,
 279     author = {Cormac Flanagan and James B. Saxe},
 280     title = {Avoiding Exponential Explosion: Generating Compact Verification Conditions},
 281     booktitle = {Principles Of Programming Languages},
 282     year = 2001,
 283     pages = {193--205},
 284     publisher = {ACM}
 285 }