Automated Testing and Debugging of SAT and QBF Solvers

Robert Brummayer; Florian Lonsing; Armin Biere

doi:10.1007/978-3-642-14186-7_6

Automated Testing and Debugging of SAT and QBF Solvers

Robert Brummayer
, Florian Lonsing
, Armin Biere

Institut für Formale Modelle und Verifikation

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

Abstract

Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.

Originalsprache	Englisch
Titel	Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10)
Verlag	Springer
Seiten	44-57
Seitenumfang	14
Band	6175
ISBN (Print)	3642141854, 9783642141850
DOIs	https://doi.org/10.1007/978-3-642-14186-7_6
Publikationsstatus	Veröffentlicht - Juli 2010

Publikationsreihe

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band	6175 LNCS
ISSN (Print)	0302-9743
ISSN (elektronisch)	1611-3349

Wissenschaftszweige

102011 Formale Sprachen
102 Informatik
101 Mathematik

JKU-Schwerpunkte

Computation in Informatics and Mathematics

Zugriff auf Dokument

10.1007/978-3-642-14186-7_6

Andere Dateien und Links

http://fmv.jku.at

Dieses zitieren

Brummayer, R., Lonsing, F., & Biere, A. (2010). Automated Testing and Debugging of SAT and QBF Solvers. in Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10) (Band 6175, S. 44-57). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6175 LNCS). Springer. https://doi.org/10.1007/978-3-642-14186-7_6

@inproceedings{e9cf40c83e994d0b8f6890e8a713254c,

title = "Automated Testing and Debugging of SAT and QBF Solvers",

abstract = "Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.",

author = "Robert Brummayer and Florian Lonsing and Armin Biere",

year = "2010",

month = jul,

doi = "10.1007/978-3-642-14186-7\_6",

language = "English",

isbn = "3642141854",

volume = "6175",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "44--57",

booktitle = "Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10)",

}

Brummayer, R, Lonsing, F & Biere, A 2010, Automated Testing and Debugging of SAT and QBF Solvers. in Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10). Bd. 6175, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bd. 6175 LNCS, Springer, S. 44-57. https://doi.org/10.1007/978-3-642-14186-7_6

Automated Testing and Debugging of SAT and QBF Solvers. / Brummayer, Robert; Lonsing, Florian; Biere, Armin.
Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10). Band 6175 Springer, 2010. S. 44-57 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6175 LNCS).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

TY - GEN

T1 - Automated Testing and Debugging of SAT and QBF Solvers

AU - Brummayer, Robert

AU - Lonsing, Florian

AU - Biere, Armin

PY - 2010/7

Y1 - 2010/7

N2 - Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.

AB - Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.

UR - http://fmv.jku.at

U2 - 10.1007/978-3-642-14186-7_6

DO - 10.1007/978-3-642-14186-7_6

M3 - Conference proceedings

SN - 3642141854

SN - 9783642141850

VL - 6175

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 44

EP - 57

BT - Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10)

PB - Springer

ER -

Brummayer R, Lonsing F, Biere A. Automated Testing and Debugging of SAT and QBF Solvers. in Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10). Band 6175. Springer. 2010. S. 44-57. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-14186-7_6