Theory-Specific Proof Steps Witnessing Correctness of SMT Executions
TimeWednesday, December 8th10:52am - 11:15am PST
Event Type
Research Manuscript
Virtual Programs
Presented In-Person
Design Verification and Validation
DescriptionEnsuring hardware and software correctness increasingly relies on the use of symbolic logic solvers, in particular for satisfiability modulo theories (SMT). However, building efficient and correct SMT solvers is difficult: even state-of-the-art solvers disagree on instance satisfiability. This work presents a system for witnessing unsatisfiability of instances of NP problems, commonly appearing in verification, in a way that is natural to SMT solving. Our implementation of the system seems to often result in significantly smaller witnesses, lower solving overhead, and faster checking time in comparison to existing proof formats that can serve a similar purpose.