Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

We propose \emph{Value Mutation Testing}, a novel approach for testing SMT solvers. The core idea behind this technique is to generate test cases by mutating the constant values within a given seed SMT formula. We further develop a strategy, \emph{Boolean Expression Coercion} (BEC), for systematically choosing value mutations. BEC extracts value mutations from the model of a separate SMT solver call that leverages constraints derived from the original seed formula. We realized Value Mutation Testing via BEC in a prototype tool: ValFuzz. In a preliminary evaluation with ValFuzz, we have already uncovered and confirmed 11 new bugs in the comprehensively tested, state-of-the-art SMT solvers, Z3 and CVC4. Developers of these solvers greatly appreciated our bug reports. We further demonstrate with ValFuzz, using a set of known bugs, that BEC is an effective method for picking value mutations. In the future, we aim at a more thorough evaluation of Value Mutation Testing to understand its full potential.