【10-31】1st-SKLCS Seminar on”Fast Verified SCCs for Probabilistic Model Checking”

Title: Fast Verified SCCs for Probabilistic Model Checking
Speaker: Bram Kohlen (PhD candidate, University of Twente, Netherlands)
Time: 2023年10月31号（周二），14:00
Venue: Room 337, Buiding 5, Institute of Software, Chinese Academy of Sciences
Abstract: High-performance probabilistic model checkers like the Modest Toolset’s mcsta follow the topological ordering of an MDP’s strongly connected components (SCCs) to speed up the numerical analysis. They use hand-coded and -optimised implementations of SCC-finding algorithms. Verified SCC-finding implementations so far were orders of magnitudes slower than their unverified counterparts. In this paper, we show how to use a refinement approach with the Isabelle theorem prover to formally verify an imperative SCC-finding implementation that can be swapped in for mcsta’s current unverified one. It uses the same state space representation as mcsta, avoiding costly conversions of the representation. We evaluate the verified implementation’s performance using an extensive benchmark, and show that its use does not significantly influence mcsta’s overall performance. Our work exemplifies a practical approach to incrementally increase the trustworthiness of existing model checking software by replacing unverified components with verified versions of comparable performance.
Bio: Bram Kohlen is currently a PhD student at the University of Twente under supervision of Arnd Hartmanns, Peter Lammich and Marieke Huisman. His research interests include verified probabilistic verification, that is, formal development of trustworthy probabilistic model checkers by intereactive theorem provers. More information can be found at https://people.utwente.nl/b.kohlen.