Previous Up Next

References

[1]
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Proceedings of the 23rd international conference on Computer aided verification, CAV’11, pages 171–177, Berlin, Heidelberg, 2011. Springer-Verlag.
[2]
Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer-Verlag, 2004.
[3]
François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 1–5, 2008.
[4]
Sylvain Conchon and Évelyne 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.
[5]
Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy. Instrumenting a weakest precondition calculus for counterexample generation. Journal of Logical and Algebraic Methods in Programming, 99:97–113, 2018.
[6]
Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger 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.
[7]
David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in SPARK. In Rocco De Nicola and Eva Kühn, editors, Software Engineering and Formal Methods, Lecture Notes in Computer Science, pages 215–233, Vienna, Austria, 2016.
[8]
Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.
[9]
Andrei 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.
[10]
Natarajan Shankar and Peter 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