State extensions for java pathfinder

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

Abstract

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.

BibTeX

@inproceedings{Gvero-al:ICSE08,
  author    = {Tihomir Gvero and
               Milos Gligoric and
               Steven Lauterburg and
               Marcelo d'Amorim and
               Darko Marinov and
               Sarfraz Khurshid},
  title     = {State extensions for java pathfinder},
  booktitle = {ICSE},
  pages     = {863--866},
  publisher = {{ACM}},
  year      = {2008},
}

State extensions for java pathfinder

Abstract

Related papers