Commit f5ee5c23 authored by Joachim Bard's avatar Joachim Bard
Browse files

Merge remote-tracking branch 'upstream/master'

parents 6e4f45f1 123de65a
# Project FloVer # Project FloVer
## FM 2019 ## Interval Subdivisions and SMT-based range analysis
All implementations included in the FM2019 submission are on the branch [FM19][2]. Interval subdivisions and SMT-based range analysis are implemented on the branch [SMT_Subdiv][2].
The folder `scripts` contains the scripts we used to run the evaluation from the paper. The folder `scripts` contains the scripts we used to evaluate the new features.
Changes described in the paper can be found in the folder `coq`. The overall soundness theorem is stated in file `CertificateChecker.v`. 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]. 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 ## FMCAD 2018
...@@ -114,6 +114,6 @@ We would like to thank Jacques-Henri Jourdan for the many insightful discussions ...@@ -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. and technical help while working on the initial version of FloVer.
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018 [1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FM19 [2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/SMT_Subdiv
[3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SMTValidation.v [3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/SMT_Subdiv/coq/SMTValidation.v
[4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SubdivsChecker.v [4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/SMT_Subdiv/coq/SubdivsChecker.v
\ No newline at end of file \ No newline at end of file
Subproject commit 78f69d7fcdd795890f213134d66582ece116e14b Subproject commit 7acebe9f434d9882401f73a0d4a14e9e5e4844a8
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