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
Fuzzing and Delta-Debugging SMT Solvers
Sprache des Titels:
Proc. 7th Intl. Workshop on Satisfiability Modulo Theories (SMT'09)
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.