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.