Model-Based API Testing for SMT Solvers

Verification back ends such as SMT solvers are typically highly complex pieces of software with performance, correctness and robustness as key requirements. Full verification of SMT solvers, however, is difficult due to their complex nature and still an open question. Grammar-based black-box input fuzzing proved to be effective 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 effective 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 effective for testing SMT solvers.