Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving

ABAD, PABLO; AGUIRRE, NAZARENO; BENGOLEA, VALERIA; CIOLEK, DANIEL; FRIAS, MARCELO FABIAN; GALEOTTI, JUAN PABLO; MAIBAUM, THOMAS STEPHEN EDWARD; MOSCATO, MARIANO MIGUEL; ROSNER, NICOLÁS; VISSANI, IGNACIO

Luxemburgo

Conferencia; IEEE Sixth International Conference on Software Testing, Verification and Validation; 2013

IEEE

In this article we present a novel and general tech- nique for automated test generation that combines tight TACO bounds with incremental SAT solving. The synergy produced from combining these techniques allows us to generate test inputs more efficiently than current state-of-the-art tools. The generality of the proposed technique allows us to generate tests according both to black-box and white-box testing criteria. As we will show through a number of experiments using our prototype tool FAJITA, the technique is particularly effective when testing classes with rich contracts.