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.
Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:00 - 17:00
|Go2Pins: a framework for the LTL verification of Go programs|
|C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs|
|Probabilistic Model Checking of Randomized Java Code|