Fast machine words in Isabelle/HOL

DOI10.1007/978-3-319-94821-8_23OpenAlexW2810581008MaRDI QIDQ1791180

Andreas Lochbihler

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_23

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver, Primitive Floats in Coq, A verified implementation of the Berlekamp-Zassenhaus factorization algorithm

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• JavaFAN
• PVS
• Maude
• CeTA
• CakeML
• HOL-TestGen
• Fiat
• GRAT
• CertiCoq