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 programmi...
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2021
|