manual.bib 7.71 KB
Newer Older
1
@comment{{This file has been generated by bib2bib 1.94}}
MARCHE Claude's avatar
MARCHE Claude committed
2

3
@comment{{Command line: /usr/bin/bib2bib -c '$key="schulz04ijcar" or $key="ayad10ijcar" or $key="CoqArt" or $key="conchon08smt" or $key="paskevich09rr" or $key="z3" or $key="ergo" or $key="simplify05" or $key="DM06" or $key="BarTin-CAV-07" or $key="vstte10comp" or $key="melquiond08rnc" or $key="filliatre07cav" or $key="okasaki98" or $key="boogie11why3" 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 /home/cmarche/biblio/crossrefs2.bib}}
MARCHE Claude's avatar
MARCHE Claude committed
4

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{lnai = {Lecture Notes in Artificial Intelligence}}
MARCHE Claude's avatar
MARCHE Claude committed
8

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

11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
@inproceedings{BarTin-CAV-07,
  author = {Clark Barrett and Cesare Tinelli},
  title = {{CVC3}},
  booktitle = {Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), Berlin, Germany},
  pages = {},
  year = 2007,
  editor = {W.~Damm and H.~Hermanns},
  volume = {},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarTin-CAV-07.pdf}
}

@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},
  serie = {Texts in Theoretical Computer Science},
  year = 2004
}

@unpublished{DM06,
  author = {Bruno Dutertre and Leonardo de Moura},
  institution = {SRI International},
  title = {The {Yices} {SMT} Solver},
  year = {2006},
  note = {available at \url{http://yices.csl.sri.com/tool-paper.pdf}}
}

@article{simplify05,
  author = {David Detlefs and
               Greg Nelson and
               James B. Saxe},
  title = {Simplify: a theorem prover for program checking.},
  journal = {J. ACM},
  volume = {52},
  number = {3},
  year = {2005},
  pages = {365-473},
  ee = {http://doi.acm.org/10.1145/1066100.1066102},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@misc{z3,
  author = {Leonardo de Moura and Nikolaj Bj{\o}rner},
  title = {{Z3}, An Efficient {SMT} Solver},
  note = {\url{http://research.microsoft.com/projects/z3/}}
}

61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
@inproceedings{schulz04ijcar,
  author = {S. Schulz},
  title = {{System Description: E~0.81}},
  booktitle = {Proc.\ of the 2nd IJCAR, Cork, Ireland},
  editor = {D. Basin and M. Rusinowitch},
  volume = 3097,
  series = {LNAI},
  year = 2004,
  publisher = {Springer},
  pages = {223--228}
}

@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},
  note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}
}

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

MARCHE Claude's avatar
MARCHE Claude committed
90 91
@inproceedings{conchon08smt,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
MARCHE Claude's avatar
MARCHE Claude committed
92
  and St\'ephane Lescuyer},
MARCHE Claude's avatar
MARCHE Claude committed
93 94
  title = {{Implementing Polymorphism in SMT solvers}},
  booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
MARCHE Claude's avatar
MARCHE Claude committed
95
  pages = {1--5},
MARCHE Claude's avatar
MARCHE Claude committed
96 97 98
  year = 2008,
  editor = {Clark Barrett and Leonardo de Moura},
  volume = 367,
MARCHE Claude's avatar
MARCHE Claude committed
99
  series = {ACM International Conference Proceedings Series},
MARCHE Claude's avatar
MARCHE Claude committed
100
  topics = {team,lri},
MARCHE Claude's avatar
MARCHE Claude committed
101
  type_digiteo = {conf_autre},
MARCHE Claude's avatar
MARCHE Claude committed
102
  type_publi = {colloque},
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106 107 108 109 110 111 112 113 114
  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}
}

115 116 117 118
@misc{ergo,
  author = {Sylvain Conchon and \'Evelyne Contejean},
  title = {The {Alt-Ergo} automatic Theorem Prover},
  url = {http://alt-ergo.lri.fr/},
119 120
  howpublished = {\url{http://alt-ergo.lri.fr/}},
  note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
121 122 123 124 125 126 127
  topics = {team,lri},
  year = 2008,
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}

MARCHE Claude's avatar
MARCHE Claude committed
128 129 130
@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
131 132 133 134 135 136 137 138 139 140 141 142 143 144
  Verification},
  crossref = {cav07},
  pages = {173--177},
  topics = {team, lri},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  x-equipes = {demons PROVAL EXT},
  x-type = {articlecourt},
  x-support = {actes},
  x-cle-support = {CAV}
}

145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
@inproceedings{melquiond08rnc,
  author = {Guillaume Melquiond},
  title = {Floating-point arithmetic in the {C}oq system},
  booktitle = {Proceedings of the 8th Conference on Real Numbers and Computers},
  address = {Santiago de Compostela, Spain},
  year = {2008},
  pages = {93--102},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RNC},
  topics = {team},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
160
  x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
161 162
}

MARCHE Claude's avatar
MARCHE Claude committed
163 164 165 166 167 168 169 170
@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/}},
171
  number = 7128
MARCHE Claude's avatar
MARCHE Claude committed
172 173 174 175 176 177 178
}

@inproceedings{ayad10ijcar,
  author = {Ali Ayad and Claude March\'e},
  title = {Multi-Prover Verification of Floating-Point Programs},
  crossref = {ijcar10},
  url = {http://www.lri.fr/~marche/ayad10ijcar.pdf},
179
  x-equipes = {demons PROVAL EXT},
MARCHE Claude's avatar
MARCHE Claude committed
180
  topics = {team},
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  x-cle-support = {IJCAR},
  x-type = {article},
  x-editorial-board = {yes}
}

@inproceedings{boogie11why3,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
  title = {Why3: Shepherd Your Herd of Provers},
  topics = {team},
  booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
  year = 2011,
  address = {Wroc\l{}aw, Poland},
  month = {August},
  url = {http://proval.lri.fr/submissions/boogie11.pdf},
  abstract = {Why3 is the next generation of the
  Why software verification platform. 
  Why3 clearly separates the purely logical
  specification part from generation of verification conditions for programs.
  This article focuses on the former part.
  Why3 comes with a new enhanced language of
  logical specification. It features a rich library of
  proof task transformations that can be chained to produce a suitable
  input for a large set of theorem provers, including SMT solvers,
  TPTP provers, as well as interactive proof assistants.}
MARCHE Claude's avatar
MARCHE Claude committed
210
}
MARCHE Claude's avatar
MARCHE Claude committed
211

MARCHE Claude's avatar
MARCHE Claude committed
212 213 214 215 216 217 218 219 220 221
@proceedings{ijcar10,
  title = {International Joint Conference on Automated Reasoning},
  booktitle = {Fifth International Joint Conference on Automated Reasoning},
  year = 2010,
  editor = {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  address = {Edinburgh, Scotland},
  month = jul,
  series = lnai,
  publisher = sv
}
MARCHE Claude's avatar
MARCHE Claude committed
222

MARCHE Claude's avatar
MARCHE Claude committed
223 224 225
@proceedings{cav07,
  editor = {Werner Damm and Holger Hermanns},
  title = {Computer Aided Verification},
MARCHE Claude's avatar
MARCHE Claude committed
226
  booktitle = {19th International Conference on Computer Aided Verification},
MARCHE Claude's avatar
MARCHE Claude committed
227 228 229 230 231 232
  publisher = sv,
  series = lncs,
  volume = 4590,
  address = {Berlin, Germany},
  month = jul,
  year = {2007}
MARCHE Claude's avatar
MARCHE Claude committed
233
}
MARCHE Claude's avatar
MARCHE Claude committed
234