Skip to content
Snippets Groups Projects
Commit a40d99f5 authored by Heiko Becker's avatar Heiko Becker
Browse files

Update README.md

parent 6a6ee6a4
No related branches found
No related tags found
No related merge requests found
# Project FloVer
## FM 2019
## Interval Subdivisions and SMT-based range analysis
All implementations included in the FM2019 submission are on the branch [FM19][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`.
Interval subdivisions and SMT-based range analysis are implemented on the branch [SMT_Subdiv][2].
The folder `scripts` contains the scripts we used to evaluate the new features.
Our Coq implementation is 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
......@@ -114,6 +114,6 @@ 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
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FM19
[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
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/SMT_Subdiv
[3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/SMT_Subdiv/coq/SMTValidation.v
[4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/SMT_Subdiv/coq/SubdivsChecker.v
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment