Test input generation for red-black trees using abstraction
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Article in Proceedings |
| Conference | Automated Software Engineering |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | test input generation; state space exploration; state matching |
| Description | We consider the problem of test input generation for code that manipulates complex data structures. Test inputs are sequences of method calls from the data structure interface. We describe test input input generation techniques that rely on state matching to avoid generation of redundant tests. Exhaustive techniques use explicit state model checking to explore all the possible test sequences up to predefined input sizes. Lossy techniques rely on abstraction mappings to compute and store abstract versions of the concrete states they explore under-approximations of all the possible test sequences. We have implemented the technique on top of the Java PathFinder model checker and we evaluate them using a Java implementation of red-black trees. |
| Related projects: |