Probabilistic model checking of randomized Java code

Java PathFinder (JPF) and PRISM are the most popular model checkers for Java code and systems that exhibit random behaviour, respectively. Our tools make it possible to use JPF and PRISM together. For the first time, probabilistic properties of randomized algorithms implemented in a modern programming language can be checked. Furthermore, our tools are accompanied by a large collection of randomized algorithms that we implemented in Java. From those Java applications and with the help of our tools, we have generated the largest collection of realistic labelled (discrete time) Markov chains