A Why3 framework for reflection proofs and its application to GMP's algorithms

DOI10.1007/978-3-319-94205-6_13OpenAlexW2786891599MaRDI QIDQ1799078

Raphaël Rieu-Helft, Guillaume Melquiond

Publication date: 18 October 2018

Full work available at URL: https://hal.inria.fr/hal-01699754v2/file/main.pdf

zbMATH Keywords

decision proceduresdeductive program verificationnonlinear integer arithmeticproofs by reflection

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

WhyMP, a formally verified arbitrary-precision integer library ⋮ Unnamed Item

Uses Software

• Dafny
• Why3
• Leon
• Mtac

This page was built for publication: A Why3 framework for reflection proofs and its application to GMP's algorithms