Marta Kwiatkowska
Marta Zofia Kwiatkowska is a Polish theoretical computer scientist based in the United Kingdom. She is professor of computing in the Department of Computer Science at the University of Oxford, England, and a Fellow of Trinity College, Oxford.
Education
Kwiatkowska received her Bachelor of Science and Master of Science degrees in Computer Science with distinction summa cum laude from Jagiellonian University in Krakow, Poland. She obtained her PhD in Computer Science from the University of Leicester in 1989.Career and research
Between obtaining her BSc/MSc and her appointment as professor of Computing Systems at the University of Oxford in 2007, Kwiatkowska served in the following posts.- Assistant professor, Jagiellonian University, Krakow, Poland
- Research Scholar, University of Leicester
- Lecturer in Computer Science, University of Leicester
- Lecturer in Computer Science, University of Birmingham
- Reader in Semantics for Concurrency, University of Birmingham
- Professor of Computer Science, University of Birmingham
Kwiatkowska serves on editorial boards of several journals, including Information and Computation, Formal Methods in System Design, Logical Methods in Computer Science, Science of Computer Programming and the Royal Society's Open science. Her research has been supported by grant funding from EPSRC, ERC, EU, DARPA, and Microsoft Research Cambridge, including the prestigious ERC Advanced Grant VERIWARE and the EPSRC Programme Grant on Mobile Autonomy.
Kwiatkowska currently serves as Deputy Head of Department at the Department of Computer Science at Oxford, and was the department's first female professor. She is the head of the Automated Verification research theme.
Projects
- Mobile Autonomy, an ERC-funded programme grant.
- AFFECTech, funded by the EU's Horizon2020 research and innovation programme.
Selected previous research projects
- VERIWARE: From Software Verification to ‘Everyware’ Verification.
- VERIPACE: Design, Analysis and Synthesis Tools for Cardiac Pacemaker Software.
- Predictable Software Systems.
- CONNECT-IP: Emergent Connectors for Eternal Software Intensive Networked Systems.
- Automated Quantitative Software Verification with PRISM.
- UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures.
- Shaping an International Grand Challenge Community for Ubiquitous Computing.
- Predictive modelling of signalling pathways via probabilistic model checking with PRISM.
- Automated Verification of Probabilistic Protocols with PRISM.
- Probabilistic Model Checking of Mobile Ad Hoc Network Protocols.
- Verification of Quality of Service Properties in Timed Systems.
- Automatic Verification of Randomized Distributed Algorithms.
Notable contributions
- Introduced probabilistic/quantitative model checking on the international scene, and spearheaded its transition from theory to practice.
- Led the development of PRISM, the world-leading probabilistic model checker considered a landmark for research in the area, which has been downloaded over 60,000 times and won the HVC 2016 Award.
- Formulated and implemented novel frameworks for: semantic models for probabilistic systems; verification for probabilistic timed automata and probabilistic software; multi-objective model checking for probabilistic systems; software verification for sensor networks; quantitative multi-objective verification and controller synthesis for stochastic games; quantitative runtime and incremental verification; and parameter synthesis for probabilistic models.
- Developed extensive compositional assume-guarantee reasoning frameworks for component based systems modelled as interface automata, as well quantitative verification and strategy synthesis for probabilistic systems.
- Applied probabilistic verification and synthesis to a broad range of real-world systems, detecting flaws in some of them, including the Bluetooth protocol, reliability of nanotechnology designs and smartgrid demand management protocol.
- Developed an extensive model-based framework for closed-loop verification of cardiac pacemaker models against personalised heart models. The framework supports quantitative verification, personalisation and optimal timing delay synthesis for pacemaker software.
- For the first time, applied probabilistic model checking in systems biology to predict quantitative properties of the FGF signalling pathway that were later confirmed experimentally.
- Extended and applied probabilistic verification to automatically find and diagnose errors in DNA computing designs, to study computational potential and analyse reliability of DNA walker circuits, and to develop a predictive model of DNA origami folding that serves as a 'molecular breadboard' for DNA circuits in an article published in Nature.
Selected talks and lectures
- – Hay Festival talk on 30 May 2017.
- – invited talk at Computer Aided Verification 2017.
- – invited lecture at Simons Institute for the Theory of Computing, UC Berkeley, October 2016.
- – invited lecture at IntelliSys, September 2016.
- – keynote lecture at CMSB 2015.
- – keynote lecture at Petri nets 2015/ACSD 2015.
- – ACCESS Distinguished Lecture given at KTH Royal Institute of Technology in Stockholm, November 2014, based on 2012 Milner Lecture, University of Edinburgh.
- – 2012 Milner Lecture, University of Edinburgh, September 2012.
- – keynote lecture at ATVA 2013, Hanoi, Vietnam.
- – a talk given at Algorithmic Bioprocesses 2007.
- – invited talk at LICS 2003, Ottawa.
- at POPL 2015.
- , 4th Summer School on Formal Techniques in Atherton, California, 2014.
Committee memberships
- Member, Presburger Award, since 2016.
- Member, Computer Aided Verification Award Panel, 2010 – 2014.
- Chair, European Research Council Starting Grants Panel, 2012 – 2016.
- Member, Research Excellence Framework 2014 Subpanel 11.
- Member, Royal Society Dorothy Hodgkin Fellowships Panel, since 2012.
- Member, Vienna Science Technology Fund Panel, 2012 and 2015.
- Member, Dutch Informatics Review Panel, 2009.
Awards and honours
- Elected a Fellow of the Royal Society in 2019.
- Milner Award 2018.
- Fellow of European Association for Theoretical Computer Science, elected 2017.
- Fellow of the Association for Computing Machinery, elected 2016 for "fundamental contributions to the theory and practice of probabilistic verification and its applications.”
- Haifa Verification Conference Award 2016, joint with Dave Parker and Gethin Norman, "for the invention, development and maintenance of the PRISM probabilistic model checker."
- honorary Doctorate, KTH Royal Institute of Technology, 2014, awarded for being "the driving force for the development of probabilistic and quantitative methods within computer science.”
- Elected to give the 2012 Milner Lecture at the University of Edinburgh, awarded for "excellent and original theoretical work which has a perceived significance for practical computing.”
- Member of Academia Europaea, elected 2011
- Fellow of British Computer Society, elected 2008.
Personal life