Theory-Specific Proof Steps Witnessing Correctness of SMT Executions

Title:

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions

Authors:

R. Otoni, M. Blicha, P. Eugster, A. Hyvärinen, N. Sharygina

Publication:

58th ACM/IEEE Design Automation Conference (DAC)

DOI:

Year:

2021

Abstract:

Ensuring 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.

BibTeX:

@inproceedings{otoni_theoryspecific_2021,
    title = {{Theory-Specific Proof Steps Witnessing Correctness of SMT Executions}},
    author = {Otoni, Rodrigo and Blicha, Martin and Eugster, Patrick and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2021},
    booktitle = {{58th ACM/IEEE Design Automation Conference (DAC)}},
    doi = {10.1109/DAC18074.2021.9586272},
    pages = {541--546},
}