ase2011 Arcaini, Paolo Gargantini, Angelo Riccobene, Elvinia

Optimizing the Automatic Test Generation by SAT and SMT solving for Boolean Expressions

in 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, USA (Eds. Perry Alexander and Corina S. Pasareanu and John G. Hosking) , IEEE (2011): 388 -391 ISBN 978-1-4577-1638-6

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]

My sw links