Robert Brummayer, Armin Biere,
"Fuzzing and Delta-Debugging SMT Solvers"
, in Bruno Dutertre und Ofer Strichman: Proc. 7th Intl. Workshop on Satisfiability Modulo Theories (SMT'09), Seite(n) 3-13, 8-2009
Original Titel:
Fuzzing and Delta-Debugging SMT Solvers
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 7th Intl. Workshop on Satisfiability Modulo Theories (SMT'09)
Original Kurzfassung:
SMT solvers are widely used as core engines in many applications. Therefore,
robustness and correctness are essential criteria. Current testing techniques used
by developers of SMT solvers do not satisfy the high demand for correct and robust
solvers, as our testing experiments show. To improve this situation, we propose to
complement traditional testing techniques with grammar-based blackbox fuzz testing,
combined with delta-debugging. We demonstrate the effectiveness of our approach
and report on critical bugs and incorrect results which we found in current
state-of-the-art SMT solvers for bit-vectors and arrays.
Forschungs-