State extensions for java pathfider

Tihomir Gvero, Milos Gligoric, Steven Lauterburg, d'Amorim Marcelo d'Amorim, Darko Marinov, Sarfraz Khurshid

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationICSE'08
Subtitle of host publicationProceedings of the 30th International Conference on Software Engineering 2008
Number of pages4
StatePublished - 2008
Event30th International Conference on Software Engineering 2008, ICSE'08 - Leipzig, Germany
Duration: May 10 2008May 18 2008

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257


Other30th International Conference on Software Engineering 2008, ICSE'08


  • Delta execution
  • JPF
  • Java pathfinder
  • Mixed execution

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'State extensions for java pathfider'. Together they form a unique fingerprint.

Cite this