Hammering Floating-Point Arithmetic
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- A Brief Overview of HOL4
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A Skeptic's approach to combining HOL and Maple
- A formally verified, optimized monitor for metric first-order dynamic logic
- ATP and presentation service for Mizar formalizations
- Automating the verification of floating-point programs
- Combining superposition, sorts and splitting
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- Fast LCF-Style Proof Reconstruction for Z3
- Faster, higher, stronger: E 2.3
- Formal Methods for Hardware Verification
- HOL(y)Hammer: online ATP service for HOL Light
- Handbook of Floating-Point Arithmetic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Lightweight relevance filtering for machine-generated resolution problems
- Mizar: state-of-the-art and beyond
- Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications
- Superposition for higher-order logic
- Towards satisfiability modulo parametric bit-vectors
This page was built for publication: Hammering Floating-Point Arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6496632)
