A GDB-like debugger for programs running under Java Pathfinder
Java ANTLR
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
bin
doc
documentation
lib
src
tools
ATTRIBUTION.txt
LICENSE-2.0.txt
README.md
build.xml
jpf.properties
symbolic-execution-support.jpf

README.md

JPF Inspector is a debugging tool for Java Pathfinder. You may attach the JPF Inspector to a program run using the Java Pathfinder virtual machine to debug it and step through it. It supports breakpoints and single-step execution (forward and backward) at different levels of granularity, and it allows the user to examine and modify program state (threads, call stacks, and heap objects). Unlike with standard debuggers (GDB), it is also possible to control thread scheduling explicitly.

Java Pathfinder (JPF) is a framework for formal checking of Java programs. Its core consists of a virtual machine for Java bytecode, running itself on Java; this allows JPF to instrument the code and provide its own functionality for critical instructions. JPF is very extensible and many modules exist for various kinds of verification such as symbolic execution. JPF Inspector is one such JPF module that focuses on debugging capability.

Quick Start

This project has an extensive documentation at this repository's GitHub wiki.

You could start with the following articles:

The User Guide also contains instructions on how to install JPF Inspector into your system.