Close

Presentation

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions
TimeWednesday, December 8th10:52am - 11:15am PST
Location3016
Event Type
Research Manuscript
Virtual Programs
Presented In-Person
Keywords
Design Verification and Validation
Topics
EDA
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.