biblio

doc/manpages.tex

@@ -63,6 +63,7 @@ definitions~\cite{paskevich09rr}
 \item[encoding\_enumeration]
 \item[encoding\_simple2]
 \item[encoding\_smt]
+Should we cite \cite{conchon08smt} here?
 \item[encoding\_tptp]
 \item[filter\_trigger]
 \item[filter\_trigger\_builtin]

doc/manual.bib

+
+
+
+@string{SV = "Springer"}
+
+
+@string{lncs = "Lecture Notes in Computer Science"}
+
+@InProceedings{conchon08smt,
+  author = 	 {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
+  and St\'ephane Lescuyer},
+  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}
+}
+
+@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/},
+  number =    {RR-7128}}
+
+
+@InProceedings{filliatre07cav,
+  author = 	 {Jean-Christophe Filli\^atre and Claude March\'e},
+  title = 	 {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
+  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}
+}
+
+
+
+@Proceedings{cav07,
+  editor    = {Werner Damm and Holger Hermanns},
+  title     = {Computer Aided Verification},
+  booktitle = {19th International Conference on Computer Aided Verification},
+  publisher = SV,
+  series    = lncs,
+  volume    = 4590,
+  address   = {Berlin, Germany},
+  month     = jul,
+  year      = {2007}
+}

doc/manual.tex

 \documentclass[a4paper]{memoir}
 
-%\usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
 \usepackage{url}
-\usepackage{ocamldoc}
 
+% for ocamldoc generated pages
+\usepackage{ocamldoc}
 \let\tt\ttfamily
 \let\bf\bfseries
 
+
 \begin{document}
 
-\title{Why3 manual}
-\author{F. Bobot \and J.-C. Filli\^atre \and C. March\'e \and A. Paskevich}
-\maketitle
+\thispagestyle{empty}
+
+\begin{center}
+
+~
+
+\vfill
+
+{\Huge\bfseries Why3 manual}
+
+\vfill
+
+{\Large F. Bobot$^{1,2}$ \\ 
+J.-C. Filli\^atre$^{2,1}$  \\ 
+C. March\'e$^{3,1}$ \\ 
+A. Paskevich$^{1,2}$}
+
+\vfill
+
+\begin{tabular}{l}
+$^1$ Univ Paris-Sud, Orsay, F-91405 \\
+$^2$ LRI, CNRS, Orsay, F-91405 \\
+$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893 
+\end{tabular}
+
+\vfill
+
+\begin{flushleft}
+  \textcopyright 2010-2010 Univ Paris-Sud, CNRS, INRIA
+
+  This work has been supported by the `U3CAT' national ANR project
+  (ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the
+  Hi-Lite (\url{http://www.open-do.org/projects/hi-lite/}) FUI project of the
+  System@tic competitivity cluster.
+
+\end{flushleft}
+\end{center}
 
 \cleardoublepage
 
 \tableofcontents
 
+\chapter*{Foreword}
+
+This is the manual for the Why platform version 3, or Why3 for
+short. Why3 is a complete reimplementation of the former Why
+platform~\cite{filliatre07cav} for program verification.  The major
+change is a completely new design of the architecture for calling
+external provers. An important emphasis is put on the genericity,
+which allows for the end user to easily add the support for a new
+external prover if wanted.  An major new feature is also the ability
+to use Why programmatically, via an well-defined API.
+
+\section*{Acknowledgements}
+
+We gratefully thank all the people who contributed to this document:
+
 \input{syntax.tex}
 
 \input{ide.tex}