David Parker
Professor of Computer Science, University of Oxford
David Parker
David Parker
Department of Computer Science
University of Oxford
Wolfson Building, 
Parks Road,
Oxford, OX1 3QD
+44 1865 283528
Room 424
Find me on:

I'm a Professor of Computer Science at the University of Oxford and a Tutorial Fellow at Trinity College.

From Oct 2021, I am also a Turing Fellow.

Research

My research is in formal verification: rigorous techniques for checking that systems function correctly. In particular, I work on quantitative verification methods for checking properties such as safety, reliability, robustness and performance.

I am particularly interested in verification methods for establishing the correctness and robustness of AI-based systems, and work on techniques and tools for providing formally guaranteed solutions to problems across sequential decision making, multi-agent systems and neuro-symbolic systems.

PRISM

I lead the development of PRISM, the most widely-used software tool for verification of probabilistic systems. It was originally created as part of my PhD thesis. See here for some pointers about PRISM, or browse the publications and some applications. We have also developed PRISM-games, an extension of the tool for verifying stochastic games.

I am interested in many aspects of the verification of probabilistic systems. In particular, I currently work on robust verification techniques which can quantify epistemic uncertainty, especially in the context of learning-based systems, and verification of multi-agent systems using stochastic games. I'm interested in applying both to the formal verification and control of AI-driven systems such as robotics and autonomous systems.

Take a look at my papers and talks to find out more.

If you are interested in undertaking a PhD or student project in any of these areas, please get in touch.

News & Activities [show all]

Projects

Current research projects:

Previous research projects:

Other projects funding PRISM:

People

PhD students:


Post-docs:


Events

I am currently on the programme committee for the following events. Please consider submitting a paper.

I am also on the editorial board for:

Some previous programme committees:

    • 2023
    • SETTA 2023 (Intl. Symposium on Dependable Software Engineering)
    • QEST 2023 (Intl. Conference on Quantitative Evaluation of SysTems)
    • AAAI 2023 (AAAI Conference on Artificial Intelligence)
    • 2022
    • FORMATS 2022 [PC co-chair] (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
    • QEST 2022 (Intl. Conference on Quantitative Evaluation of SysTems)
    • AAAI 2022 (AAAI Conference on Artificial Intelligence)
    • MARS 2022 (Intl. Workshop on Models for Formal Analysis of Real Systems)
    • SETTA 2022 (Intl. Symposium on Dependable Software Engineering)
    • 2021
    • TACAS 2021 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    • RV 2021 (Intl. Conference on Runtime Verification)
    • HSCC 2021 (Intl. Conference on Hybrid Systems: Computation and Control)
    • AAAI 2021 (AAAI Conference on Artificial Intelligence)
    • FM 2021 (Intl. Conference on Formal Methods)
    • QEST 2021 (Intl. Conference on Quantitative Evaluation of SysTems)
    • SETTA 2021 (Intl. Symposium on Dependable Software Engineering)
    • R2AW 2021 (Robust and Reliable Autonomy in the Wild)
    • SYNT 2021 (Intl. Workshop on Synthesis)
    • EPEW 2021 (European Performance Engineering Workshop)
    • TOSME 2021 (Intl. Workshop on Tools for Stochastic Modelling and Evaluation)
    • 2020
    • TACAS 2020 [PC co-chair] (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    • QEST 2020 (Intl. Conference on Quantitative Evaluation of SysTems)
    • AAAI 2020 (AAAI Conference on Artificial Intelligence)
    • SETTA 2020 (Intl. Symposium on Dependable Software Engineering)
    • IJCAI-PRICAI 2020 (Intl. Joint Conference on Artificial Intelligence & Pacific Rim Intl. Conference on Artificial Intelligence)
    • MARS 2020 (Intl. Workshop on Models for Formal Analysis of Real Systems)
    • InterAVT 2020 (Interactive Workshop on the Industrial Application of Verification and Testing)
    • 2019
    • QEST 2019 [PC co-chair] (Intl. Conference on Quantitative Evaluation of SysTems)
    • TACAS 2019 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    • IJCAI 2019 (Intl. Joint Conference on Artificial Intelligence)
    • FT4DAS 2019 (Intl. Workshop on Formal Techniques for Dependable Autonomous Systems)
    • InterAVT 2019 (Interactive Workshop on the Industrial Application of Verification and Testing)
    • 2018
    • TACAS 2018 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    • IJCAI 2018 (Intl. Joint Conference on Artificial Intelligence)
    • FORMATS 2018 (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
    • ICECCS 2018 (Intl. Conference On Engineering Of Complex Computer Systems)
    • VaVaS 2018 (Intl. Workshop on Verification and Validation of Autonomous Systems)
    • 2017
    • InfQ 2017 (Intl. Workshop on Quantitative Methods in Informatics)
    • TACAS 2017 [Tools chair] (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    • LATA 2017 (Intl. Conference on Language and Automata Theory and Applications)
    • MARS 2017 (Intl. Workshop on Models for Formal Analysis of Real Systems)
    • 2016
    • CAV 2016 (Intl. Conference on Computer Aided Verification)
    • FORMATS 2016 (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
    • VMCAI 2016 (Intl. Conference on Verification, Model Checking, and Abstract Interpretation)
    • PASM 2016 (Intl. Workshop on Practical Applications of Stochastic Modelling)
    • 2015
    • CAV 2015 (Intl. Conference on Computer Aided Verification)
    • TACAS 2015 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    • SEFM 2015 (Intl. Conference on Software Engineering and Formal Methods)
    • CTSE 2015 (Intl. Workshop on Control Theory for Software Engineering)
    • VMCAI 2015 (Intl. Conference on Verification, Model Checking, and Abstract Interpretation)
    • QEST 2015 (Intl. Conference on Quantitative Evaluation of SysTems)
    • QAPL 2015 (Intl. Workshop on Quantitative Aspects of Programming Languages)
    • 2014
    • QEST 2014 [Tools chair] (Intl. Conference on Quantitative Evaluation of SysTems)
    • FORMATS 2014 (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
    • SPIN 2014 (Intl. SPIN Symposium on Model Checking of Software)
    • HPCC 2014 (IEEE Intl. Conference on High Performance Computing and Communications)
    • VEMDP 2014 (Intl. Workshop on Verification of Engineered Molecular Devices and Programs)
    • SEFM 2014 (Intl. Conference on Software Engineering and Formal Methods)
    • FMICS 2014 (Intl. Workshop on Formal Methods for Industrial Critical Systems)
    • QAPL 2014 (Intl. Workshop on Quantitative Aspects of Programming Languages)
    • PASM 2014 (Intl. Workshop on Practical Applications of Stochastic Modelling)
    • GRAPHITE 2014 (Intl. Workshop on Graph Inspection and Traversal Engineering)
    • SIMUTools 2014 (Intl. Conference on Simulation Tools and Techniques)
    • 2013
    • CONCUR 2013 (Intl. Conference on Concurrency Theory)
    • TASE 2013 (Intl. Symposium on Theoretical Aspects of Software Engineering)
    • SPIN 2013 (Intl. SPIN Symposium on Model Checking of Software)
    • CBSE 2013 (Intl. ACM SIGSOFT Symposium on Component-Based Software Engineering)
    • FMICS 2013 (Intl. Workshop on Formal Methods for Industrial Critical Systems)
    • HAS 2013 (Intl. Workshop on Hybrid Autonomous Systems)
    • SIMUTools 2013 (Intl. Conference on Simulation Tools and Techniques)
    • GRAPHITE 2013 (Intl. Workshop on Graph Inspection and Traversal Engineering)
    • FAMES 2013 (Intl. Workshop on Formal Approaches to Managing Evolving Systems)
    • QAPL 2013 (Intl. Workshop on Quantitative Aspects of Programming Languages)
    • SAC 2013-COSYS [PC co-chair] (ACM Symposium on Applied Computing: Cooperative Systems)
    • SAC 2013-SVT (ACM Symposium on Applied Computing: Software Verification & Testing)
    • 2012
    • CMSB 2012 (Intl. Conference on Computational Methods in Systems Biology)
    • SPIN 2012 [PC co-chair] (Intl. SPIN Workshop on Model Checking of Software)
    • PASM 2012 (Intl. Workshop on Practical Applications of Stochastic Modelling)
    • FMICS 2012 (Intl. Workshop on Formal Methods for Industrial Critical Systems)
    • SIMUTools 2012 (Intl. Conference on Simulation Tools and Techniques)
    • QAPL 2012 (Intl. Workshop on Quantitative Aspects of Programming Languages)
    • SAC 2012-SVT (ACM Symposium on Applied Computing, Software Verification & Testing)
    • SAC 2012-COSYS [PC co-chair] (ACM Symposium on Applied Computing)