Theory-Specific Proof Steps Witnessing Correctness of SMT Executions

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

2021 58th ACM/IEEE Design Automation Conference (DAC)

ISBN

978-1-66543-275-7

ISSN

0738-100X

e-ISSN

—

Počet stran výsledku

6

Strana od-do

541-546

Název nakladatele

IEEE

Místo vydání

San Francisco, CA, USA

Místo konání akce

San Francisco, California, United States

Datum konání akce

5. 12. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—