References
-
[1]
-
IEEE standard for floating-point arithmetic, 2008.
doi:10.1109/IEEESTD.2008.4610935.
- [2]
-
Y. Bertot and P. Castéran.
Interactive Theorem Proving and Program Development.
Texts in Theoretical Computer Science. Springer-Verlag, 2004.
doi:10.1007/978-3-662-07964-5.
- [3]
-
F. Bobot, S. Conchon, E. Contejean, and S. Lescuyer.
Implementing polymorphism in SMT solvers.
In C. Barrett and L. de Moura, editors, SMT 2008: 6th
International Workshop on Satisfiability Modulo, volume 367 of ACM
International Conference Proceedings Series, pages 1–5, 2008.
doi:10.1145/1512464.1512466.
- [4]
-
S. Conchon and E. Contejean.
The Alt-Ergo automatic theorem prover, 2008.
URL: http://alt-ergo.lri.fr/.
- [5]
-
D. Detlefs, G. Nelson, and J. B. Saxe.
Simplify: a theorem prover for program checking.
Journal of the ACM, 52(3):365–473, 2005.
doi:10.1145/1066100.1066102.
- [6]
-
J.-C. Filliâtre and C. Marché.
The Why/Krakatoa/Caduceus platform for deductive program
verification.
In W. Damm and H. Hermanns, editors, 19th International
Conference on Computer Aided Verification, volume 4590 of Lecture Notes
in Computer Science, pages 173–177, Berlin, Germany, July 2007. Springer.
doi:10.1007/978-3-540-73368-3_21.
- [7]
-
D. Hauzar, C. Marché, and Y. Moy.
Counterexamples from proof failures in SPARK.
In R. De Nicola and E. Kühn, editors, Software Engineering and
Formal Methods, Lecture Notes in Computer Science, pages 215–233, Vienna,
Austria, 2016.
doi:10.1007/978-3-319-41591-8_15.
- [8]
-
C. Okasaki.
Purely Functional Data Structures.
Cambridge University Press, 1998.
- [9]
-
A. Paskevich.
Algebraic types and pattern matching in the logical language of the
Why verification platform.
Technical Report 7128, INRIA, 2009.
URL: http://hal.inria.fr/inria-00439232.
- [10]
-
N. Shankar and P. Mueller.
Verified Software: Theories, Tools and Experiments (VSTTE’10).
Software Verification Competition, August 2010.
URL: http://www.macs.hw.ac.uk/vstte10/Competition.html.