Sciweavers

Share
PTS
2010

Test Data Generation for Programs with Quantified First-Order Logic Specifications

8 years 8 months ago
Test Data Generation for Programs with Quantified First-Order Logic Specifications
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....
Christoph Gladisch
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where PTS
Authors Christoph Gladisch
Comments (0)
books