Test Data Generation For Programs with Quantified First-order Logic
Specifications
Christoph Gladisch
We present a novel algorithm for test data generation that is based on
techniques used in formal software verification. Prominent examples of such
formal techniques are symbolic execution, theorem proving, satisfiability
solving, and usage of specifications and program annotations such as loop
invariants. These techniques are suitable for testing of small programs,
such as, e.g., implementations of algorithms, that have to be tested
extremely well.
In such scenarios test data is generated from test data constraints which
are first-order logic formulas. These constraints are constructed from path
conditions, specifications, and program annotation describing program paths
that are hard to be tested randomly. A challenge is, however, to solve
quantified formulas. The presented algorithm is capable of solving
quantified formulas that state-of-the-art satisfiability modulo theory (SMT)
solvers cannot solve. The algorithm is integrated in the formal verification
and test generation tool KeY .