Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
Abstract elided by the publisher.
Related papers
- Foundational Multi-Modal Program Verifiers POPL 2026
- Veil: A Framework for Automated and Interactive Verification of Transition Systems CAV 2025
- Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean CAV 2026
- Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers TACAS 2020
- A Formalization of Core Why3 in Coq POPL 2024
- The Vampire Diary CAV 2025
- lean-smt: An SMT Tactic for Discharging Proof Goals in Lean CAV 2025
- SMTScope: Automated and Efficient Analysis of SMT Traces TACAS 2026