Publication details
Test input generation for red
-black trees using abstraction
| Basic information | |
|---|---|
| Original title: | Test input generation for red-black trees using abstraction |
| Authors: | Radek Pelánek, Corina Pasareanu, Willem Visser |
| Further information | |
|---|---|
| Citation: | PELÁNEK, Radek - PASAREANU, Corina - VISSER, Willem. Test input generation for red-black trees using abstraction. In Automated Software Engineering. USA : ACM, 2005. pp. 414-417. 2005, Long Beach, California. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | test input generation; state space exploration; state matching |
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:
- Automated Verification of Parallel and Distributed Systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
