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 Assistent 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.
