Many methods in data structures contain a loop structure on a collection type. These loops result in a large number of test cases and are one of the main obstacles to systematically test these methods. To deal with the loops in methods, in this paper, we propose a novel loop-extended model checking approach, abbreviated as LEMC, to efficiently test whether methods satisfy their own invariant. Our main idea is to combine dynamic symbolic execution with static analysis techniques. Specifically, a concrete execution of the method under test is initially done to collect dynamic execution information, which is used to statically identify the loop-extended similar paths of the concrete execution path. LEMC statically checks and prunes all the states which follow these loop-extended similar paths. The experiments on several case studies show that LEMC can dramatically reduce as many as 90% of the search space and achieve much better performance, compared with the existing approaches such as the Glass Box model checker and Korat. © 2011 Springer-Verlag.
CITATION STYLE
Yi, Q., Liu, J., & Shen, W. (2011). Efficient loop-extended model checking of data structure methods. In Communications in Computer and Information Science (Vol. 257 CCIS, pp. 237–249). https://doi.org/10.1007/978-3-642-27207-3_24
Mendeley helps you to discover research relevant for your work.