B. Kohlen MSc (Bram)

Sinds januari 2021 werk ik aan het project "Verified Probabilistic Verification". Er zijn verschillende manieren om systemen en software te testen. Model Checking is een zulke manier. Mijn interesse ligt daarbij vooral bij het testen van systemen die willekeurig gedrag vertonen. Deze kunnen we verifiëren met "Probabilistic Model Checking". Een van de belangrijkste algoritmes blijkt echter foutief te zijn. Ik probeer het vertrouwen in onze methodes te herstellen door onze algoritmes correct te bewijzen in de theorem prover Isabelle/HOL. Met het Isabelle Refinement Framework wil ik deze bewijzen vertalen naar uitvoerbare code die bestaande implementaties kan valideren en zelfs snel genoeg is om geïntegreerd te worden in de model checkers zoals de Modest Toolset.

Verbonden aan

• Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools (FMT)