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.
Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions / P. Arcaini, A. Gargantini, E. Riccobene - In: 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)[s.l] : IEEE, 2011. - ISBN 9781457716393. - pp. 388-391 (( Intervento presentato al 26. convegno Automated Software Engineering (ASE) tenutosi a Lawrence, Kansas nel 2011 [10.1109/ASE.2011.6100079].
Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions
P. ArcainiPrimo
;E. RiccobeneUltimo
2011
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.File | Dimensione | Formato | |
---|---|---|---|
ase11_SATSMT_short.pdf
accesso aperto
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
585 kB
Formato
Adobe PDF
|
585 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.