Commit 5f9b2016 authored by MARCHE Claude's avatar MARCHE Claude

Doc: updated section 5.3 on Why3 IDE

parent f1efc9bf
This diff is collapsed.
@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}}
@string{sv = {Springer}}
@string{lncs = {Lecture Notes in Computer Science}}
......@@ -12,24 +16,29 @@
doi = {10.1007/978-3-662-07964-5}
}
@article{simplify05,
author = {David Detlefs and Greg Nelson and James B. Saxe},
title = {Simplify: a theorem prover for program checking.},
journal = {Journal of the ACM},
volume = {52},
number = {3},
year = {2005},
pages = {365--473},
doi = {10.1145/1066100.1066102},
}
@misc{ieee754-2008,
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.},
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}
year = {2008},
note = {\url{https://dx.doi.org/10.1109/IEEESTD.2008.4610935}}
}
@misc{vstte10comp,
......@@ -39,7 +48,7 @@
month = {August},
year = 2010,
address = {Edinburgh, Scotland},
url = {http://www.macs.hw.ac.uk/vstte10/Competition.html}
note = {\url{http://www.macs.hw.ac.uk/vstte10/Competition.html}}
}
@book{okasaki98,
......@@ -49,24 +58,60 @@
year = 1998
}
@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}
}
@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},
abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
}
@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,
......@@ -75,6 +120,15 @@
Verification},
crossref = {cav07},
pages = {173--177},
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},
doi = {10.1007/978-3-540-73368-3_21}
}
......@@ -83,11 +137,14 @@
title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
institution = {INRIA},
year = 2009,
url = {http://hal.inria.fr/inria-00439232},
topics = {team},
hal = {http://hal.inria.fr/inria-00439232},
note = {\url{http://hal.inria.fr/inria-00439232}},
number = 7128
}
@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},
......@@ -97,6 +154,20 @@
editor = {De Nicola, Rocco and Eva K\"uhn},
series = lncs,
address = {Vienna, Austria},
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}
}
@proceedings{cav07,
......@@ -111,18 +182,3 @@
year = {2007}
}
@inproceedings{cvc4,
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},
}
......@@ -20,7 +20,7 @@ requires to import the theory of integer arithmetic from the \why
standard library, which is done by the \texttt{use} declaration above.
We don't give more details here about the syntax and refer to
Chapter~\ref{chap:syntax} for detailed explanations. In the following,
Chapter~\ref{chap:whyml} for detailed explanations. In the following,
we show how this file is handled in the \why GUI
(Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}
executable (Section~\ref{sec:batch}).
......@@ -248,7 +248,7 @@ Known provers:
\index{list-provers@\verb+--list-provers+}
The first word of each line
is a unique identifier for the associated prover. We thus have now the
three provers Alt-Ergo~\cite{ergo}, CVC4~\cite{cvc4}, and
three provers Alt-Ergo~\cite{ergo}, CVC4~\cite{barrett11cade}, and
Coq~\cite{CoqArt}.
Let us assume that we want to run Alt-Ergo on the HelloProof
......
......@@ -311,7 +311,7 @@ of an equivalence: \texttt{A <-> B -> C} is rejected.
\subsection{Terms}
The syntax for terms is given in Figure~\ref{fig:bnf:term}.
The syntax for terms is given in Figure~\ref{fig:bnf:term1}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
\begin{center}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment