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

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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.

Original language	English
Title of host publication	Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10)
Publisher	Springer
Pages	44-57
Number of pages	14
Volume	6175
ISBN (Print)	3642141854, 9783642141850
DOIs	https://doi.org/10.1007/978-3-642-14186-7_6
Publication status	Published - Jul 2010

Publication series

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

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

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

Cite this

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) (Vol. 6175, pp. 44-57). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 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). vol. 6175, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6175 LNCS, Springer, pp. 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). Vol. 6175 Springer, 2010. p. 44-57 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6175 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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). Vol. 6175. Springer. 2010. p. 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

Automated Testing and Debugging of SAT and QBF Solvers

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this