Commit 67607f7a authored by Heiko Becker's avatar Heiko Becker

Update README.md with latest state of FloVer

parent 6fd90de5
# Project FloVer
## FM 2019
All implementations included in the FM2019 submission are on the branch [FM2019][2].
The folder `scripts` contains the scripts we used to run the evaluation from the paper.
Changes described in the paper can be found in the folder `coq`. The overall soundness theorem is stated in file `CertificateChecker.v`.
The SMT-based range validator and its soundness proof can be found in file [SMTValidation.v][3], and the Subdivision checker can be found in file [SubdivsChecker.v][4].
## FMCAD 2018
The artifact and scripts used to run the evaluation for FMCAD 2018 can be found on the branch [FMCAD 2018][1].
......@@ -30,7 +37,7 @@ Full support for fixed-point programs is also only available in `affine_arithmet
## Checking Coq certificates
FloVer is known to compile with coq `8.7.2` and `8.8.0`.
FloVer is known to compile with coq `8.8.2`.
To check the Coq certificate, you need to enter the `coq` directory.
Place any certificate you want to have checked into the `output` folder in the
coq directory and then run
......@@ -43,9 +50,8 @@ This will compile all coq files and then in the end the certificate in the outpu
To compile the file `IEEE_connection.v` showing the relation to IEEE754 semantics, it is necessary to install
the Flocq library via opam:
```bash
$ opam install coq-flocq.2.6.1
$ opam install coq-flocq.3.1.0
```
Note that due to some incompatibilities, FloVer currently does not support flocq 3.0.
The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory.
......@@ -99,7 +105,7 @@ $ ./cake_checker CERTIFICATE_FILE
## Contributors
In no particular order: Raphael Monat, Nikita Zyuzin, Heiko Becker
In no particular order: Raphael Monat, Nikita Zyuzin, Joachim Bard, Heiko Becker
Acknowledgements
......@@ -107,4 +113,7 @@ Acknowledgements
We would like to thank Jacques-Henri Jourdan for the many insightful discussions
and technical help while working on the initial version of FloVer.
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
\ No newline at end of file
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FM2019
[3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SMTValidation.v
[4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SubdivsChecker.v
\ No newline at end of file
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