ECOOP and ISSTA 2021 (series) / SPIN 2021 (series) / 27th International SPIN Symposium on Model Checking of Software /
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
Mon 12 Jul
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:00 - 17:00 | |||
16:00 20mTalk | Go2Pins: a framework for the LTL verification of Go programs SPIN | ||
16:20 20mTalk | C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs SPIN Antoine Chenoy Université catholique de Louvain, Fabien Duchene ICTEAM, UCLouvain, Thomas Given-Wilson Université catholique de Louvain, Axel Legay Université Catholique de Louvain, Belgium | ||
16:40 20mTalk | Probabilistic Model Checking of Randomized Java Code SPIN Syyeda Zainab Fatmi York University, Xiang Chen University of Waterloo, Yash Dhamija York University, Maeve Wildes McGill University, Qiyi Tang University of Oxford, Franck van Breugel York University, Canada | ||