7th Intl. Workshop on Satisfiability Modulo Theories (SMT'09)
Sprache des Tagungstitel:
Englisch
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-