TY - GEN
T1 - State extensions for java pathfider
AU - Gvero, Tihomir
AU - Gligoric, Milos
AU - Lauterburg, Steven
AU - Marcelo d'Amorim, d'Amorim
AU - Marinov, Darko
AU - Khurshid, Sarfraz
N1 - Copyright:
Copyright 2009 Elsevier B.V., All rights reserved.
PY - 2008
Y1 - 2008
N2 - Java PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison. This paper summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.
AB - Java PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison. This paper summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.
KW - Delta execution
KW - JPF
KW - Java pathfinder
KW - Mixed execution
UR - http://www.scopus.com/inward/record.url?scp=56249124546&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=56249124546&partnerID=8YFLogxK
U2 - 10.1145/1368088.1368224
DO - 10.1145/1368088.1368224
M3 - Conference contribution
AN - SCOPUS:56249124546
SN - 9781605580791
T3 - Proceedings - International Conference on Software Engineering
SP - 863
EP - 866
BT - ICSE'08
T2 - 30th International Conference on Software Engineering 2008, ICSE'08
Y2 - 10 May 2008 through 18 May 2008
ER -