Aina Niemetz, Mathias Preiner, Armin Biere,
"Model-Based API Testing for SMT Solvers"
: Proc. 15th Intl. Workshop on Satisfiability Modulo Theories (SMT'17), Serie 15th Intl. Workshop on Satisfiability Modulo Theories, 2017
Original Titel:
Model-Based API Testing for SMT Solvers
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 15th Intl. Workshop on Satisfiability Modulo Theories (SMT'17)
Original Kurzfassung:
Veri?cation back ends such as SMT solvers are typically highly complex pieces of software with performance, correctness and robustness as key requirements. Full veri?cation of SMT solvers, however, is di?cult due to their complex nature and still an open question. Grammar-based black-box input fuzzing proved to be e?ective to uncover bugs in SMT solvers but is entirely input-based and restricted to a certain input language. State-of-theart SMT solvers, however, usually provide a rich API, which often introduces additional functionality not supported by the input language. Previous work showed that applying model-based API fuzzing to SAT solvers is more e?ective than input fuzzing. In this paper, we introduce a model-based API testing framework for our SMT solver Boolector. Our experimental results show that model-based API fuzzing in combination with delta debugging techniques is e?ective for testing SMT solvers.
Sprache der Kurzfassung:
Englisch
Serie:
15th Intl. Workshop on Satisfiability Modulo Theories
Forschungs-