jpf-prism is an extension of the Java Pathfinder (JPF) that allows users to model-check probabilistic programs. jpf-prism uses JPF to exhaustively explore the set of possible program states in a probabilistic Java program, while building a Markov chain of the system states, and then finally passing passing this chain to the PRISM model checker in order to compute the probabilities of reaching a state with a desired property in the System-Under-Test (SUT).

See the wiki for an example program being checked with jpf-prism, installation instructions, command line instructions, and how to specify system properties for jpf-prism.

Note that jpf-prism requires the use of jpf-v7.


coming soon..

Questions & Comments

Send questions and comments to


Thanks to David Parker, Neha Rungta, and Franco Raimondi for their help during the development of this extension.