Monitoring Java programs with Java PathExplorer

Klaus Havelund, Grigore Roşu

Research output: Contribution to journalConference articlepeer-review


We present recent work on the development of Java PathExplorer (JPaX), a tool for monitoring the execution of Java programs. JPaX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems. The tool facilitates automated instrumentation of a program's byte code, which will then emit events to an observer during its execution. The observer checks the events against user provided high level requirement specifications, for example temporal logic formulae, and against lower level error detection procedures, usually concurrency related such as deadlock and data race algorithms. High level requirement specifications together with their underlying logics are defined in rewriting logic using Maude, and then can either be directly checked using Maude rewriting engine, or be first translated to efficient data structures and then checked in Java.

Original languageEnglish (US)
Pages (from-to)200-217
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Issue number2
StatePublished - Oct 2001
Externally publishedYes
EventRV'2001, Runtime Verification (in Connection with CAV '01) - Paris, France
Duration: Jul 23 2001Jul 23 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Monitoring Java programs with Java PathExplorer'. Together they form a unique fingerprint.

Cite this