From January 2021 I have been working on the project "Verified Probabilistic Verification". There are a multitude of ways to verify whether systems or software work as intended. One such way is Model Checking. My interest lies in Probabilistic Model Checking which is capable of verifying systems that have random behavior. However, one of the core algorithms for this type of model checking, called value iteration, has been proven to be faulty. To restore the faith in our tools, I want to prove the correctness of these algorithms in the theorem prover "Isabelle/HOL". I use the Isabelle Refinement Framework to generate a fast correct-by-construction code. These are competitive with manually implemented and optimized implementations in existing model checkers such as the Modest Toolset.
Organisations
Research profiles
Affiliated study programs
Courses academic year 2023/2024
Courses in the current academic year are added at the moment they are finalised in the Osiris system. Therefore it is possible that the list is not yet complete for the whole academic year.
Courses academic year 2022/2023
Address
University of Twente
Zilverling (building no. 11), room 3126
Hallenweg 19
7522 NH Enschede
Netherlands
University of Twente
Zilverling 3126
P.O. Box 217
7500 AE Enschede
Netherlands
Scan the QR code or