Add missing references and clean/complete bibliography entries.

a2e998a1 · Guillaume Melquiond · 5c64f692 · a2e998a1 · a2e998a1 · a2e998a1
Commit a2e998a1 authored Nov 08, 2017 by Guillaume Melquiond
--- a/doc/fix.hva
+++ b/doc/fix.hva
@@ -5,6 +5,7 @@
 \newcommand{\vfill}{}
 \newcommand{\hrulefill}{}
 \newcommand{\null}{}
+\newcommand{\path}[1]{\texttt{#1}}
 \renewcommand{\framebox}[1]{#1}

 \makeatletter

--- a/doc/manual.bib
+++ b/doc/manual.bib
-@comment{{This file has been generated by bib2bib 1.94}}
-
-@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}}
-
 @string{sv = {Springer}}

-@string{lnai = {Lecture Notes in Artificial Intelligence}}
-
 @string{lncs = {Lecture Notes in Computer Science}}

-@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}}
+  series = {Texts in Theoretical Computer Science},
+  year = 2004,
+  doi = {10.1007/978-3-662-07964-5}
 }

 @article{simplify05,
-  author = {David Detlefs and
-               Greg Nelson and
-               James B. Saxe},
+  author = {David Detlefs and Greg Nelson and James B. Saxe},
  title = {Simplify: a theorem prover for program checking.},
-  journal = {J. ACM},
+  journal = {Journal of the 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}
+  pages = {365--473},
+  doi = {10.1145/1066100.1066102},
 }

-@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/}}
-}
-
-@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{ieee754-2008,
+  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},
+  year = {2008}
 }

 @misc{vstte10comp,
@@ -77,12 +39,12 @@
  month = {August},
  year = 2010,
  address = {Edinburgh, Scotland},
-  note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}
+  url = {http://www.macs.hw.ac.uk/vstte10/Competition.html}
 }

 @book{okasaki98,
  author = {Chris Okasaki},
-  title = {{Purely Functional Data Structures}},
+  title = {Purely Functional Data Structures},
  publisher = {Cambridge University Press},
  year = 1998
 }
@@ -90,39 +52,21 @@
 @inproceedings{conchon08smt,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
  and St\'ephane Lescuyer},
-  title = {{Implementing Polymorphism in SMT solvers}},
+  title = {Implementing Polymorphism in {SMT} solvers},
  booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
  pages = {1--5},
  year = 2008,
  editor = {Clark Barrett and Leonardo de Moura},
  volume = 367,
  series = {ACM International Conference Proceedings Series},
-  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}
+  doi = {10.1145/1512464.1512466},
 }

 @misc{ergo,
  author = {Sylvain Conchon and \'Evelyne Contejean},
  title = {The {Alt-Ergo} automatic Theorem Prover},
  url = {http://alt-ergo.lri.fr/},
-  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},
  year = 2008,
-  x-equipes = {demons PROVAL},
-  x-type = {manuel},
-  x-support = {diffusion}
 }

 @inproceedings{filliatre07cav,
@@ -131,33 +75,7 @@
  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}
-}
-
-@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},
-  x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
+  doi = {10.1007/978-3-540-73368-3_21}
 }

 @techreport{paskevich09rr,
@@ -165,59 +83,20 @@
  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/}},
+  url = {http://hal.inria.fr/inria-00439232},
  number = 7128
 }

-@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},
-  x-equipes = {demons PROVAL EXT},
-  topics = {team},
-  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.}
-}
-
-@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
+@inproceedings{hauzar16sefm,
+  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},
 }

 @proceedings{cav07,
@@ -231,37 +110,3 @@ Claude March\'e and Andrei Paskevich},
  month = jul,
  year = {2007}
 }
-
-@InProceedings{hauzar16sefm,
-  topics = {team},
-  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},
-  hal =  {https://hal.inria.fr/hal-01314885}
-}
-
-
-@techreport{ieee754-2008,
-	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.},
-	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},
-	year = {2008}
-}
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -422,9 +422,9 @@ are the following.
 % %   the future. Examples are available in \texttt{examples/programs}. *)
 % \end{itemize}

-\bibliographystyle{abbrv}
+\bibliographystyle{abbrvurl}
 \bibliography{manual}
-%\input{biblio-demons}
+%\bibliography{abbrevs,demons,demons2,demons3,team,crossrefs}


 % \cleardoublepage

--- a/doc/syntaxref.tex
+++ b/doc/syntaxref.tex
@@ -242,7 +242,7 @@ This type is used in the standard library in the theories

 A declaration of the form \texttt{type f = < float \textit{eb sb} >}
 defines a type of floating-point numbers as specified by the IEEE-754
-standard~\cite{ieee754}. Here the literal \texttt{\textit{eb}}
+standard~\cite{ieee754-2008}. Here the literal \texttt{\textit{eb}}
 represents the number of bits in the exponent and the literal
 \texttt{\textit{sb}} the number of bits in the significand (including
 the hidden bit). Note that in order to make such a declaration the