[Back]

M. Tautschnig:
"Query-Driven Program Testing";
Supervisor, Reviewer: H. Veith, D. Kroening; Institut für Informationssysteme, 2011; oral examination: 2011-04-11.

In this dissertation we describe a new method for fully automatic test case generation following formal specifications given by test engineers.
We build upon a well-defined mathematical core that captures the semantics of coverage criteria.
On top of this framework we define the declarative test specification language FQL, the FShell query language.
These formal specifications are supplemented with an engine that generates test cases in response to FQL queries.
We chose this overall design of a mathematical core, a query language and an efficient back end in analogy to databases and hence refer to our method as query-driven program testing.
The full workflow is implemented for ANSI C programs in a tool called FShell, which uses components of the C Bounded Model Checker (CBMC).