loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 International Conference on Software Testing Verification and Validation
Optimizing Generation of Object Graphs in Java PathFinder
Denver, Colorado
April 01-April 04
ISBN: 978-0-7695-3601-9
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.
Citation:
Milos Gligoric, Tihomir Gvero, Steven Lauterburg, Darko Marinov, Sarfraz Khurshid, "Optimizing Generation of Object Graphs in Java PathFinder," icst, pp.51-60, 2009 International Conference on Software Testing Verification and Validation, 2009
Usage of this product signifies your acceptance of the Terms of Use.