14. Bibliography

IEE08

IEEE standard for floating-point arithmetic. 2008. doi:10.1109/IEEESTD.2008.4610935.

BCD+11

Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In 23rd International Conference on Computer Aided Verification, 171–177. Snowbird, UT, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2032305.2032319.

Bau17

Lucas Baudin. Deductive verification with the help of abstract interpretation. Technical Report, Univ Paris-Sud, November 2017.

BFM+18

Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language. 2018. https://frama-c.com/acsl.html. URL: https://frama-c.com/acsl.html.

BC04

Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer-Verlag, 2004. doi:10.1007/978-3-662-07964-5.

BCCL08

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, 1–5. 2008. URL: http://www.lri.fr/~conchon/publis/conchon-smt08.pdf, doi:10.1145/1512464.1512466.

CC08

Sylvain Conchon and Évelyne Contejean. The Alt-Ergo automatic theorem prover. 2008. URL: http://alt-ergo.lri.fr/.

DHMM18

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. URL: https://hal.inria.fr/hal-01802488.

Filliatre07

Jean-Christophe Filliâtre. Formal Verification of MIX Programs. In Journées en l'honneur de Donald E. Knuth. Bordeaux, France, October 2007. http://knuth07.labri.fr/exposes.php. URL: http://www.lri.fr/~filliatr/publis/verifmix.pdf.

FilliatreP20

Jean-Christophe Filliâtre and Andrei Paskevich. Abstraction and genericity in why3. In Tiziana Margaria and Bernhard Steffen, editors, 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 12476 of Lecture Notes in Computer Science, 122–142. Rhodes, Greece, October 2020. Springer. URL: http://why3.lri.fr/isola-2020/.

FM07

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, 173–177. Berlin, Germany, July 2007. URL: https://hal.inria.fr/inria-00270820v1, doi:10.1007/978-3-540-73368-3_21.

HMM16

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, 215–233. Vienna, Austria, 2016. URL: https://hal.inria.fr/hal-01314885, doi:10.1007/978-3-319-41591-8_15.

Ngu12

Thi Minh Tuyen Nguyen. Taking architecture and compiler into account in formal proofs of numerical programs. PhD thesis, Université Paris-Sud, June 2012. URL: http://tel.archives-ouvertes.fr/tel-00710193.

Oka98

Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.

Pas09

Andrei 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.

SM10

Natarajan Shankar and Peter Mueller. Verified Software: Theories, Tools and Experiments (VSTTE'10). Software Verification Competition. August 2010. URL: http://www.macs.hw.ac.uk/vstte10/Competition.html.