Welcome...

B. Kohlen MSc (Bram)

PhD Candidate

About Me

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 that can be used to validate other model checkers and that can even be fast enough to be embedded in existing model checkers such as the Modest Toolset.

Google Scholar Link

Education

 

Affiliated Study Programmes

Master

Courses Academic Year  2022/2023

Contact Details

Visiting Address

University of Twente
Faculty of Electrical Engineering, Mathematics and Computer Science
Zilverling (building no. 11), room 3126
Hallenweg 19
7522NH  Enschede
The Netherlands

Navigate to location

Mailing Address

University of Twente
Faculty of Electrical Engineering, Mathematics and Computer Science
Zilverling  3126
P.O. Box 217
7500 AE Enschede
The Netherlands