Java MultiPathExplorer: (JMPaX)

Java MultiPathExplorer is a predictive safety analysis tool for Java. It analyzes a Java program in runtime and detects violation of safety properties written in past-time linear temporal logic. The tool works in two phases:
  1. First it instruments a Java program given in the form of a set of class files.
  2. Then it runs the instrumented Java program and monitors the safety property specified by the user.

The underlying theory for JMPaX can be found in the papers provided below.

JMPaX 2.0 can be downloaded from here. A user manual for the tool is yet to be written. Please see the README in the distribution to get started with JMPaX 2.0.

  1. [ps] [pdf] “Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions” Koushik Sen, Grigore Rosu and Gul Agha, In 7th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'05), LNCS (to appear).
  2. [ps] [pdf] “Instrumentation Technique for Online Analysis of Multithreaded Programs” Grigore Rosu and Koushik Sen, Special Issue of Concurrency and Computation: Practice and Experience (CC:PE) (Accepted ...)
  3. [ps] [pdf] “Online Efficient Predictive Safety Analysis of Multithreaded Programs” Koushik Sen, Grigore Rosu and Gul Agha, International Journal on Software Technology and Tools Transfer (STTT) (To Appear).
  4. [ps] [pdf] “An Instrumentation Technique for Online Analysis of Multithreaded Programs” Grigore Rosu and Koushik Sen, Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD 2004), Santa Fe, New Mexico, USA, April 2004, IEEE Digital Library Invited Paper.
  5. [ps] [pdf] “Online Efficient Predictive Safety Analysis of Multithreaded Programs” Koushik Sen, Grigore Rosu and Gul Agha, In Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 LNCS, pages 123-138, Barcelona, Spain, March 2004, Springer-Verlag. 37 papers accepted out of 145.
  6. [ps] [pdf] “Runtime Safety Analysis of Multithreaded Programs” Koushik Sen, Grigore Rosu and Gul Agha. In Proceedings of the 10th European Software Engineering Conference and the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE/ESEC 2003), pages 337-346, Helsinki, Finland, September 3-5, 2003, ACM. 33 papers accepted out of 168.
This page is maintained by Koushik Sen (ksen at cs.uiuc.edu)