Hint-Based SMT Proof Reconstruction
Abstract elided by the publisher.
Related papers
- lean-smt: An SMT Tactic for Discharging Proof Goals in Lean CAV 2025
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions CPP 2026
- Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format TACAS 2023
- Liquid proof macros Haskell 2022
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL TACAS 2024
- Laurel: Unblocking Automated Verification with Large Language Models OOPSLA 2025
- Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL CPP 2011
- System FR: formalized foundations for the stainless verifier OOPSLA 2019