Test input generation for red-black trees using abstraction

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

PELÁNEK Radek PASAREANU Corina VISSER Willem

Year of publication 2005
Type Article in Proceedings
Conference Automated Software Engineering
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.