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.
Questions & Comments
Send questions and comments to email@example.com.
Thanks to David Parker, Neha Rungta, and Franco Raimondi for their help during the development of this extension.