ABSTRACT
This paper introduces IPF-SMT, a framework that bridges the gap between SMT-based verifiers and interactive proof assistants, providing a unified intermediate proof representation, bidirectional translation, interactive debugging, and proof reconstruction to enhance software verification.
PAPER · PDF
Loading PDF...
Key findings
IPF-SMT reconstructs 89% of proofs and enables interactive completion of 67% of previously unverifiable proof obligations.
The framework reduces manual effort by 54% while maintaining full proof soundness through certified reconstruction.
Limitations & open questions
Limited diagnostic information when SMT solvers fail to discharge proof obligations.
Integrating new SMT-based verifiers with proof assistants requires substantial engineering effort.