Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
No abstract available.
DOI 10.1007/978-3-642-25379-9_15
Related papers
- Certified Connection Tableaux Proofs for HOL Light and TPTP CPP 2015
- Premise Selection and External Provers for HOL4 CPP 2015
- A Verified Compiler from Isabelle/HOL to CakeML ESOP 2018
- A Lambda-Superposition Tactic for Isabelle/HOL CPP 2026
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL TACAS 2024
- Admissible Types-to-PERs Relativization in Higher-Order Logic POPL 2023
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem CPP 2019
- lean-smt: An SMT Tactic for Discharging Proof Goals in Lean CAV 2025