Rocket-Fast Proof Checking for SMT Solvers
Abstract elided by the publisher.
Related papers
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq CPP 2011
- Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format TACAS 2023
- Automatic Abstraction in SMT-Based Unbounded Software Model Checking CAV 2013
- Making Formulog Fast: An Argument for Unconventional Datalog Evaluation OOPSLA 2024
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL TACAS 2024
- Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver VMCAI 2026
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses CPP 2011
- Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants TACAS 2006