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.
Organisaties
Onderzoeksprofielen
Verbonden aan opleidingen
Vakken collegejaar 2024/2025
Vakken in het huidig collegejaar worden toegevoegd op het moment dat zij definitief zijn in het Osiris systeem. Daarom kan het zijn dat de lijst nog niet compleet is voor het gehele collegejaar.
Scan de QR-code of