Previous Up Next

References

[1]
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.
[2]
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.
[3]
S. Conchon and E. Contejean. The Alt-Ergo automatic theorem prover. http://alt-ergo.lri.fr/, 2008. APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000.
[4]
D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365–473, 2005.
[5]
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.
[6]
D. Hauzar, C. Marché, and Y. Moy. Counterexamples from proof failures in SPARK. In Software Engineering and Formal Methods, pages 215–233, 2016.
[7]
C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.
[8]
A. Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. Technical Report 7128, INRIA, 2009. http://hal.inria.fr/inria-00439232/en/.
[9]
N. Shankar and P. Mueller. Verified Software: Theories, Tools and Experiments (VSTTE’10). Software Verification Competition, August 2010. http://www.macs.hw.ac.uk/vstte10/Competition.html.

Previous Up Next