Mark Kattenbelt
|
Mr
Mark
Kattenbelt
Room 452, Wolfson Building, Parks Road, Oxford OX1 3QD |
Interests
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.
Biography
Since July 2007 I am a Research Assistant at the Oxford University Computing Laboratory. 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.
Links
Selected Publications
| Abstraction Refinement for Probabilistic Software M. Kattenbelt‚ M. Kwiatkowska‚ G. Norman and D. Parker In Proc. 10th International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI ‘09). Springer. January, 2009. Details | BibTeX | Link (pdf) |
| 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. Details | BibTeX | Link (pdf) |
Info
|
Themes |
|
|
Activities |
Probabilistic Model Checking | Software Model Checking | Quantitative Analysis and Verification | PRISM |
|
Projects |
|
|
Supervisor |