We present a new approach to program testing which enables the programmer to specify test suites in terms of a versatile query
language. Our query language subsumes standard coverage criteria ranging from simple basic block coverage all the way to predicate
complete coverage and multiple condition coverage, but also facilitates on-the-fly requests for test suites specific to the
code structure, to external requirements, or to ad hoc needs arising in program understanding/exploration. The query language
is supported by a model checking backend which employs the CBMC framework. Our main algorithmic contribution is a method called
iterative constraint strengthening which enables us to solve a query for an arbitrary coverage criterion by a single call to the model checker and a novel form
of incremental SAT solving: Whenever the SAT solver finds a solution, our algorithm compares this solution against the coverage
criterion, and strengthens the clause database with additional clauses which exclude redundant new solutions. We demonstrate
the scalability of our approach and its ability to compute compact test suites with experiments involving device drivers,
automotive controllers, and open source projects.
Supported by DFG grant FORTAS – Formal Timing Analysis Suite for Real Time Programs (VE 455/1-1).