David Parker
Senior Lecturer, University of Birmingham
David Parker
+44 (0) 121 41 47264
Room 107 (office hours: Mon 11-12, Thur 4-5)
Find me on:
NEWS

2-3 year postdoc position available now. Contact me for details.

I'm a Senior Lecturer in Computer Science at the University of Birmingham. I also hold a Visiting Lecturer position at the University of Oxford.

Research

My research is in verification: formal techniques for checking that systems function correctly. In particular, I work on quantitative verification, which is used to check quantitative properties such as safety, reliability, performance and many others. See here for a short introduction to the topic.

This involves building and analysing models with probabilistic and real-time behaviour. I work on novel techniques to improve the scalability of verification (e.g. abstraction, compositionality), game-theoretic verification methods, and applications of these techniques to a variety of areas, including robotics, computer security, systems biology and DNA computing.

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

PRISM

I also lead the development of PRISM, the most widely-used software tool for verification of probabilistic systems. See here or here to read about PRISM, or download it and take the online tutorial.

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

News & Activities [show all]

Projects

Current research projects:

Previous research projects:

Other projects funding PRISM:

People

PhD students:

Post-docs:

Former PhD students:

Events

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

Some previous programme committees:
    • 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)
    • 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)
    • 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)
    • SIMUTools 2014 (Intl. Conference on Simulation Tools and Techniques)
    • GRAPHITE 2014 (Intl. Workshop on Graph Inspection and Traversal Engineering)
    • 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 [co-chair] (ACM Symposium on Applied Computing: Cooperative Systems)
    • SAC 2013-SVT (ACM Symposium on Applied Computing: Software Verification & Testing)
    • CMSB 2012 (Intl. Conference on Computational Methods in Systems Biology)
    • SPIN 2012 [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 [co-chair] (ACM Symposium on Applied Computing)
    • QEST 2011
    • SPIN 2011
    • SAC 2011
    • SIMUTools 2011
    • MASCOTS 2011
    • QAPL 2011
    • PASM 2011
    • SPIN 2010
    • MASCOTS 2010
    • HiBi 2010
    • QAPL 2010
    • FIT 2010
    • SOCA 2009
    • MASCOTS 2009
    • HiBi 2009
    • PASM 2009
    • TiSto 2009
    • ASHEs 2009
    • QEST 2008
    • CMSB 2008
    • PASM 2008
    • ASHEs 2008
    • FMICS 2007