manual.bib 6.68 KB
Newer Older
1 2 3 4
@comment{{This file has been generated by bib2bib 1.98}}

@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}}

MARCHE Claude's avatar
MARCHE Claude committed
5
@string{sv = {Springer}}
MARCHE Claude's avatar
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
@string{lncs = {Lecture Notes in Computer Science}}
MARCHE Claude's avatar
MARCHE Claude committed
8

9 10 11 12 13
@book{CoqArt,
  author = {Yves Bertot and Pierre Cast\'eran},
  title = {Interactive Theorem Proving and Program Development},
  subtitle = {Coq'Art: The Calculus of Inductive Constructions},
  publisher = {Springer-Verlag},
14 15 16
  series = {Texts in Theoretical Computer Science},
  year = 2004,
  doi = {10.1007/978-3-662-07964-5}
17 18
}

19
@misc{ieee754-2008,
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
  key = {IEEE754},
  abstract = {This standard specifies interchange and arithmetic
                  formats and methods for binary and decimal
                  floating-point arithmetic in computer programming
                  environments. This standard specifies exception
                  conditions and their default handling. An
                  implementation of a floating-point system conforming
                  to this standard may be realized entirely in
                  software, entirely in hardware, or in any
                  combination of software and hardware. For operations
                  specified in the normative part of this standard,
                  numerical results and exceptions are uniquely
                  determined by the values of the input data, sequence
                  of operations, and destination formats, all under
                  user control.},
35 36 37 38 39
  booktitle = {{IEEE} Std 754-2008},
  doi = {10.1109/IEEESTD.2008.4610935},
  journal = {IEEE Std 754-2008},
  pages = {1--58},
  title = {{IEEE} Standard for Floating-Point Arithmetic},
40 41
  year = {2008},
  note = {\url{https://dx.doi.org/10.1109/IEEESTD.2008.4610935}}
42 43 44 45 46 47 48 49 50
}

@misc{vstte10comp,
  author = {Natarajan Shankar and Peter Mueller},
  title = {{Verified Software: Theories, Tools and Experiments
                  (VSTTE'10). Software Verification Competition}},
  month = {August},
  year = 2010,
  address = {Edinburgh, Scotland},
51
  note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}
52 53 54 55
}

@book{okasaki98,
  author = {Chris Okasaki},
56
  title = {Purely Functional Data Structures},
57 58 59 60
  publisher = {Cambridge University Press},
  year = 1998
}

61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
@inproceedings{barrett11cade,
  author = {Barrett, Clark and Conway, Christopher L. and Deters, Morgan and Hadarean, Liana and Jovanovi\'{c}, Dejan and King, Tim and Reynolds, Andrew and Tinelli, Cesare},
  title = {{CVC4}},
  booktitle = {Proceedings of the 23rd international conference on Computer aided verification},
  series = {CAV'11},
  year = 2011,
  isbn = {978-3-642-22109-5},
  location = {Snowbird, UT},
  pages = {171--177},
  numpages = 7,
  url = {http://dl.acm.org/citation.cfm?id=2032305.2032319},
  acmid = 2032319,
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg}
}

MARCHE Claude's avatar
MARCHE Claude committed
77 78
@inproceedings{conchon08smt,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
MARCHE Claude's avatar
MARCHE Claude committed
79
  and St\'ephane Lescuyer},
80
  title = {{Implementing Polymorphism in SMT solvers}},
MARCHE Claude's avatar
MARCHE Claude committed
81
  booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
MARCHE Claude's avatar
MARCHE Claude committed
82
  pages = {1--5},
MARCHE Claude's avatar
MARCHE Claude committed
83 84 85
  year = 2008,
  editor = {Clark Barrett and Leonardo de Moura},
  volume = 367,
MARCHE Claude's avatar
MARCHE Claude committed
86
  series = {ACM International Conference Proceedings Series},
87 88 89 90 91 92 93 94 95 96 97 98 99
  topics = {team,lri},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {SMT},
  x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
  url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  isbn = {978-1-60558-440-9},
100
  doi = {10.1145/1512464.1512466},
101
  abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
MARCHE Claude's avatar
MARCHE Claude committed
102 103
}

104 105 106 107
@misc{ergo,
  author = {Sylvain Conchon and \'Evelyne Contejean},
  title = {The {Alt-Ergo} automatic Theorem Prover},
  url = {http://alt-ergo.lri.fr/},
108 109 110
  howpublished = {\url{http://alt-ergo.lri.fr/}},
  note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
  topics = {team,lri},
111
  year = 2008,
112 113 114
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
115 116
}

MARCHE Claude's avatar
MARCHE Claude committed
117 118 119
@inproceedings{filliatre07cav,
  author = {Jean-Christophe Filli\^atre and Claude March\'e},
  title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
MARCHE Claude's avatar
MARCHE Claude committed
120 121 122
  Verification},
  crossref = {cav07},
  pages = {173--177},
123 124 125 126 127 128 129 130 131
  topics = {team, lri},
  hal = {https://hal.inria.fr/inria-00270820v1},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  x-equipes = {demons PROVAL EXT},
  x-type = {articlecourt},
  x-support = {actes},
  x-cle-support = {CAV},
132
  doi = {10.1007/978-3-540-73368-3_21}
133 134
}

MARCHE Claude's avatar
MARCHE Claude committed
135 136 137 138 139
@techreport{paskevich09rr,
  author = {Andrei Paskevich},
  title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
  institution = {INRIA},
  year = 2009,
140 141 142
  topics = {team},
  hal = {http://hal.inria.fr/inria-00439232},
  note = {\url{http://hal.inria.fr/inria-00439232}},
143
  number = 7128
MARCHE Claude's avatar
MARCHE Claude committed
144 145
}

146
@inproceedings{hauzar16sefm,
147
  topics = {team},
148 149 150 151 152 153 154 155 156
  author = {Hauzar, David and March\'e, Claude and Moy, Yannick},
  title = {Counterexamples from Proof Failures in {SPARK}},
  booktitle = {Software Engineering and Formal Methods},
  year = 2016,
  pages = {215--233},
  doi = {10.1007/978-3-319-41591-8_15},
  editor = {De Nicola, Rocco and Eva K\"uhn},
  series = lncs,
  address = {Vienna, Austria},
157 158 159 160 161 162 163 164 165 166 167 168 169 170
  hal = {https://hal.inria.fr/hal-01314885}
}

@article{dailler18jlamp,
  topics = {team},
  title = {Instrumenting a Weakest Precondition Calculus for Counterexample Generation},
  author = {Dailler, Sylvain and Hauzar, David and March{\'e}, Claude and Moy, Yannick},
  hal = {https://hal.inria.fr/hal-01802488},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  publisher = {Elsevier},
  volume = 99,
  pages = {97--113},
  year = 2018,
  keywords = {Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples}
MARCHE Claude's avatar
MARCHE Claude committed
171
}
MARCHE Claude's avatar
MARCHE Claude committed
172

MARCHE Claude's avatar
MARCHE Claude committed
173 174 175
@proceedings{cav07,
  editor = {Werner Damm and Holger Hermanns},
  title = {Computer Aided Verification},
MARCHE Claude's avatar
MARCHE Claude committed
176
  booktitle = {19th International Conference on Computer Aided Verification},
MARCHE Claude's avatar
MARCHE Claude committed
177 178 179 180 181 182
  publisher = sv,
  series = lncs,
  volume = 4590,
  address = {Berlin, Germany},
  month = jul,
  year = {2007}
MARCHE Claude's avatar
MARCHE Claude committed
183
}
184