Abstract
Recent advances in propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers are increasingly rendering
SAT and SMT-based automatic test generation an attractive alternative to traditional algorithmic test generation methods.
The use of SAT/SMT solvers is particularly appealing when testing Boolean expressions: These tools are able to deal with constraints
over the models, generate compact test suites, and they support fault-based test generation methods. However, these solvers
normally require more time and greater amount of memory than classical test generation algorithms, limiting their applicability.
In this paper we propose several ways to optimize the process of test generation and we compare several SAT/SMT solvers and
propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard
methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.
[download the pdf file] [DOI] [Try the tool at http://fmse.di.unimi.it/atgtBoolean.html]