My DPhil subject concerns quantitative model checking of software. Software model checking is an established field, but focuses exclusively on qualitative properties, in order to verify the functional requirements of the program. I am interested in verifying quantitative properties, such as those found in probabilistic model checking, in order to check non-functional requirements. Hence, my research interests include:
Probabilistic model checking. In particular model checking of discrete-time models with both probabilistic and non-deterministic choice (e.g. Markov Decision Processes).
Software model checking. Explicit-state, symbolic and bounded methods. I am focusing mostly on predicate abstraction and counterexample-guided abstraction refinement, but am also interested in other general developments in the field of model checking.
Since July 2007 I am a Research Assistant at the Department of Computer Science, University of Oxford. I am also a Research Student at Oxford with Trinity College.
Before I came to Oxford I was a Research Fellow and part-time PhD student at the School of Computer Science at the University of Birmingham. Prior to this I did my MSc and BSc at the Faculty of Electrical Engineering, Mathematics and Computer Science at the University of Twente in the Netherlands.
I am a member of the Quantitative Analysis and Verification group at Oxford. Like other members of this group, I am one of the developers of the model checker PRISM. The project I am working on is Automated Quantitative Software Verification with PRISM. My supervisor is Prof. Marta Kwiatkowska.
Abstraction Refinement for Probabilistic Software
G. Norman M. Kattenbelt M. Kwiatkowska and D. Parker
In Proc. 10th International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI ‘09). Springer. January, 2009.
Verification and Refutation of Probabilistic Specifications via Games
M. Kattenbelt and M. Huth
In Proc. 29th International Conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS ‘09). 2009.
Abstraction Framework for Markov Decision Processes and PCTL via Games
Mark Kattenbelt and Michael Huth
No. RR−09−01. Oxford University Computing Laboratory. 2009.