Test input generation for red-black trees using abstraction.
Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering(2005)
摘要
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 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 techniques on top of the Java PathFinder model checker and we evaluate them using a Java implementation of red-black trees.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络