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

[BFM+18]

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

[BBLM21]

Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Explaining counterexamples with giant-step assertion checking. In José Creissac Campos and Andrei Paskevich, editors, 6th Workshop on Formal Integrated Development Environments (F-IDE 2021), Electronic Proceedings in Theoretical Computer Science. May 2021. URL: https://hal.inria.fr/hal-03217393, doi:10.4204/EPTCS.338.10.

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

[Fil07]

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.

[FGP16]

Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. URL: https://hal.archives-ouvertes.fr/hal-01256434v3.

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

[FP20]

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. See also http://why3.lri.fr/isola-2020/. URL: https://hal.inria.fr/hal-02696246.

[FS01]

Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In Principles Of Programming Languages, 193–205. ACM, 2001.

[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. Thèse de Doctorat, 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.