TY - GEN
T1 - Optimizing generation of object graphs in java pathfinder
AU - Gligoric, Milos
AU - Gvero, Tihomir
AU - Lauterburg, Steven
AU - Marinov, Darko
AU - Khurshid, Sarfraz
N1 - Copyright:
Copyright 2019 Elsevier B.V., All rights reserved.
PY - 2009
Y1 - 2009
N2 - Java PathFinder (JPF) is a popular model checker for Java programs. JPF was used to generate object graphs as test inputs for object-oriented programs. Specifically, JPF was used as an implementation engine for the Korat algorithm. Korat takes two inputs-a Java predicate that encodes properties of desired object graphs and a bound on the size of the graph-and generates all graphs (within the given bound) that satisfy the encoded properties. Korat uses a systematic search to explore the bounded state space of object graphs. Korat search was originally implemented in JPF using a simple instrumentation of the Java predicate. However, JPF is a general-purpose model checker and such direct implementation results in an unnecessarily slow search. We present our results on speeding up Korat search in JPF. The experiments on ten data structure subjects show that our modifications of JPF reduce the search time by over an order of magnitude.
AB - Java PathFinder (JPF) is a popular model checker for Java programs. JPF was used to generate object graphs as test inputs for object-oriented programs. Specifically, JPF was used as an implementation engine for the Korat algorithm. Korat takes two inputs-a Java predicate that encodes properties of desired object graphs and a bound on the size of the graph-and generates all graphs (within the given bound) that satisfy the encoded properties. Korat uses a systematic search to explore the bounded state space of object graphs. Korat search was originally implemented in JPF using a simple instrumentation of the Java predicate. However, JPF is a general-purpose model checker and such direct implementation results in an unnecessarily slow search. We present our results on speeding up Korat search in JPF. The experiments on ten data structure subjects show that our modifications of JPF reduce the search time by over an order of magnitude.
UR - https://www.scopus.com/pages/publications/67650114107
UR - https://www.scopus.com/pages/publications/67650114107#tab=citedBy
U2 - 10.1109/ICST.2009.52
DO - 10.1109/ICST.2009.52
M3 - Conference contribution
AN - SCOPUS:67650114107
SN - 9780769536019
T3 - Proceedings - 2nd International Conference on Software Testing, Verification, and Validation, ICST 2009
SP - 51
EP - 60
BT - Proceedings - 2nd International Conference on Software Testing, Verification, and Validation, ICST 2009
PB - IEEE Computer Society
T2 - 2nd International Conference on Software Testing, Verification, and Validation, ICST 2009
Y2 - 1 April 2009 through 4 April 2009
ER -