My research is concerned with modelling and analysis methods for complex systems, such as those arising in computer networks, electronic devices and biological organisms. The analysis methods that I investigate include simulation and formal verification, and particularly automatic verification (aka model checking). My work spans the whole spectrum, from theory, through algorithms to software implementation and applications.
The main focus of my research over the past several years has been on modelling and verification of probabilistic systems, which has included both theoretical investigation that resulted in new models and efficient verification algorithms, as well as practical implementation using symbolic model checking techniques. This has culminated in the development of the PRISM model checker, which is widely used for the verification of real-world case studies, ranging from correctness of security protocols, efficiency of wireless protocols, reliability of nanotechnology designs, to the analysis of signalling pathways.
Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. Prior to this she was Professor in the School of Computer Science at the University of Birmingham, Lecturer at the University of Leicester and Assistant Professor at the Jagiellonian University in Cracow, Poland. She holds a BSc/MSc in Computer Science from the Jagiellonian University, MA from Oxford and a PhD from the University of Leicester.
Marta Kwiatkowska is a Fellow of the BCS. She is a member of EPSRC Computing College and BBSRC EBS Committee. She serves on the Steering Committee of the International Conference on Quantitative Evaluation of SysTems (QEST), Editorial Board of Journals Logical Methods in Computer Science (LMCS) and Transactions on Computational Systems Biology, and is guest co-editor of the Special Issue of IEEE Transactions on Software Engineering on Quantitative Evaluation of Computer Systems. She is lead organisers of the Royal Society Discussion Meeting "From computers to ubiquitous computing, by 2020" and guest co-editor of the associated Proceedings to appear in Phil. Trans. R. Soc. A.
Marta Kwiatkowska spearheaded the development of probabilistic and quantitative methods in verification on the international scene. Her work on the theory to practice transfer of probabilistic model checking was recognised by invitation to speak at the LICS 2003 and ESEC/FSE 2007 conferences. The PRISM model checker is the leading software tool in the area and is widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology.
