Theory-Specific Proof Steps Witnessing Correctness of SMT Executions
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F21%3A10434988" target="_blank" >RIV/00216208:11320/21:10434988 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1109/DAC18074.2021.9586272" target="_blank" >https://doi.org/10.1109/DAC18074.2021.9586272</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/DAC18074.2021.9586272" target="_blank" >10.1109/DAC18074.2021.9586272</a>
Alternative languages
Result language
angličtina
Original language name
Theory-Specific Proof Steps Witnessing Correctness of SMT Executions
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
2021 58th ACM/IEEE Design Automation Conference (DAC)
ISBN
978-1-66543-275-7
ISSN
0738-100X
e-ISSN
—
Number of pages
6
Pages from-to
541-546
Publisher name
IEEE
Place of publication
San Francisco, CA, USA
Event location
San Francisco, California, United States
Event date
Dec 5, 2021
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—