Fuzzing and verifying RAT refutations with deletion information
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
Abstract
Contemporary SAT solvers emit proofs of unsatisfiability in the DRAT format to guarantee correctness of their answers. Therefore, correctness of SAT solvers is reduced to correctness of DRAT checkers, which are relatively small programs that decide whether a DRAT refutation is correct. We present a new fuzzing technique that automatically finds bugs in DRAT checkers by comparing the outputs of two DRAT checkers. In case their outputs are different a mechanically verified DRAT checker finally decides which checker has given the correct answer. Experiments show that our method finds bugs in available checkers, and also demonstrate that a common design choice in efficient DRAT checkers is inconsistent with the specification.
Details
Originalsprache | Englisch |
---|---|
Titel | FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference |
Herausgeber (Verlag) | AAAI Press |
Seiten | 190-193 |
Seitenumfang | 4 |
ISBN (elektronisch) | 978-157735787-2 |
Publikationsstatus | Veröffentlicht - 2017 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 85029531980 |
---|