David Parker
Professor of Computer Science, University of Birmingham
|
+44 (0) 121 41 43739
Room 133
|
Find me on:
|
|
I'm a Professor of 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.
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.
My research 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 and autonomous systems, computer security, systems biology and DNA computing.
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]
-
Oct 2019:
Attending Dagstuhl seminar
"Analysis of Autonomous Mobile Collectives in Complex Physical Environments".
-
Sep 2019:
Welcome to new PhD student Dan Fentham,
working on the NCSC/GCHQ-sponsored "Adversarially-robust neural networks for cyber security" project.
-
July 2019:
New paper to appear at ESORICS 2019
on automated detection of side channels in probabilistic systems, including the SCH-IMP tool, which builds upon PRISM-pomdps.
-
July 2019:
We have finalised the programme for QEST 2019.
There are some great invited talks, tutorials and papers.
Please attend! Details http://www.qest.org/qest2019/program.html.
-
July 2019:
New paper to appear at FM 2019
on verifying stochastic games using Nash equilibria.
-
July 2019:
New paper to appear at FM 2019
on verifying numerical stability properties of Kalman filters.
-
June 2019:
I'm giving an invited talk on "Multi-objective Reasoning with Probabilistic Model Checking" at MoRe 2019
(Multi-objective Reasoning in Verification and Synthesis)
in Vancouver.
-
June 2019:
I'll be PC co-chair of TACAS 2020
with Armin Biere,
to be held in Dublin in April 2020. Submit your papers!
-
May 2019:
PRISM-games version 2.1 is now available,
providing simpler installation/compilation,
updates from PRISM 4.5 and more.
More information here.
-
May 2019:
New paper to appear in IJRR (International Journal of Robotics Research) on
"Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots", with Fatma Faruq, Nick Hawes and Bruno Lacerda.
-
Apr 2019:
PRISM 4.5 is now available,
including a wide range of updates and fixes for users and developers.
More information here.
-
Mar 2019:
Mark Ryan and I have a
fully-funded PhD position on
"adversarially-robust neural networks for cyber security"
sponsored by GCHQ and the National Cyber Security Centre (NCSC).
See here for details and to apply.
-
Feb 2019:
New paper in Nature Scientific Reports
describing work on a mitotic spindle assembly checkpoint
case study using techniques developed on the
HIERATIC project.
-
Jan 2019:
The Quantitative Verification Benchmark Set is a new set of benchmarks for probabilistic model checking across a range of probabilistic models, complementing the existing
PRISM Benchmark Suite
. See our TACAS'19 paper for details.
-
Jan 2019:
New paper "Software Adaptation for an Unmanned Undersea Vehicle" in IEEE Software giving a high level overview of work on the
DARPA-funded
PRINCESS project.
-
Jan 2019:
PRISM just competed in QComp 2019: the inaugural Comparison of Tools for the Analysis of Quantitative Formal Models. See our report to appear at TACAS'19 as part of Toolympics.
-
Sep 2018:
I'll be co-chairing QEST 2019
(Intl. Conference on Quantitative Evaluation of SysTems), to held in Glasgow next September, with
Verena Wolf and
Gethin Norman.
Please submit your papers!
-
Sep 2018:
At the 2018 Highlights of Logic, Games and Automata conference in Berlin, giving an invited talk on
"Probabilistic Model Checking: Advances and Applications"
-
Aug 2018:
Our paper "Using Probabilistic Model Checking for Dynamic Power Management" is one of 5 selected to "highlight important developments for the scientific community" as part of the 30-year anniversary of the journal Formal Aspects of Computing.
-
Aug 2017:
New paper to appear at IROS 2018 on
multi-robot task allocation and planning under uncertainty, with Fatma Faruq, Nick Hawes and Bruno Lacerda.
-
May 2018:
Two new PRISM-games papers:
(i) one on an extension for concurrent stochastic games, to appear at QEST 2018;
(ii) an extended tool paper
in STTT summarising the tool and its applications.
-
Apr 2018:
Congratulations to Nishan Kamaleson, who successfully completed his PhD on
"Model Reduction Techniques for Probabilistic Verification of Markov Chains".
-
Sep 2017:
Welcome to new PhD students Edoardo Bacci and James Kelly
-
Jul 2017:
Version 4.4 of PRISM is
out now,
including interval iteration (see this CAV'17 paper),
topological iteration, new reward operators, CTL/LTL model checking and
much more.
-
Jun 2017:
Congratulations to Ahmed Al-Ajeli, who successfully defended his PhD thesis
"Fourier-Motzkin Methods for Fault Diagnosis in Discrete Event Systems" this week.
-
Jun 2017:
New paper to appear at CAV 2017 on
building a more reliable probabilistic model checker with
interval iteration.
-
May 2017:
New book chapter
on advances and applications in probabilistic model checking, to appear in the forthcoming
Formal System Verification
-
April 2017:
New paper to appear at ICAPS 2017 on
probabilistic time-bounded guarantees for mobile robots.
-
Mar 2017:
Welcome to new postdoc Chris Novakavic,
working on the DARPA-funded
PRINCESS project.
-
Feb 2017:
Welcome to new PhD student Fatma Faruq.
-
Feb 2017:
New paper to appear at CCGrid 2017 on
verification of cloud-based auto-scaling policies.
-
Jan 2017:
A 2-3 year postdoc position is available to work with me at Birmingham
on formal verification for probabilistic systems,
under the DARPA-funded BRASS program. Details here.
Contact me for details.
-
Nov 2016:
At HVC 2016 in Haifa, for the HVC award.
Presentation:
"Probabilistic Model Checking: Past, Present & Future".
-
Sep 2016:
Welcome to new PhD students Michael Oxford and Irfan Muhammad.
-
Aug 2016:
I'm Tools Chair for TACAS 2017.
Submit your tool papers now!
-
Jul 2016:
I've been awarded, jointly with Marta Kwiatkowska and Gethin Norman,
the 2016 HVC award
for "the invention, development and maintenance of the PRISM probabilistic model checker".
For more details, see here.
-
Jul 2016:
I'm hiring a postdoc and a PhD student to work on a new project
under the DARPA-funded BRASS program. This will be advertised shortly. Please contact me directly for details.
-
Jun 2016:
I'm giving a tutorial with Nick Hawes
at the ICAPS'16 summer school next week
on "Formal Guarantees for Robotic Navigation Planning", in the session
"Task Scheduling and Execution for Long-Term Autonomy".
-
Jun 2016:
New paper on verification
and strategy synthesis for attack-defence trees,
appearing at CSF'16 this month.
-
Feb 2016:
PRISM has been selected to participate in
Google Summer of Code 2016.
Contribute to PRISM and get paid for it!
See here for details if you're interested.
-
Feb 2016:
New paper on finite-horizon probabilistic bisimulation
to appear at SPIN'16.
-
Dec 2015:
Version 2.0 of PRISM-games is out,
featuring multi-objective and compositional strategy synthesis.
See our TACAS'16 paper for details.
-
Nov 2015:
Seminar at the University of Southampton:
"Probabilistic Model Checking and Strategy Synthesis".
-
Oct 2015:
Lecture at the AVACS Autumn School in Oldenburg:
"Probabilistic Model Checking and Controller Synthesis".
-
Sep 2015:
I'll be contributing to the panel "Agent Verification: Current Research Challenges"
at the the Agent Verification Workshop
in Liverpool this week.
-
Jul 2015:
PRISM now officially supports
the new Hanoi Omega-Automata format.
See our CAV'15 paper for details.
-
Jun 2015:
New paper on partially observable probabilistic real-time systems,
to appear in FORMATS 2015.
-
Jun 2015:
Congratulations to Mateusz Ujma,
who just successfully defended his thesis "On Verification and Controller Synthesis for Probabilistic Systems at Runtime".
-
May 2015:
Talk at the Autonomous Intelligent Machines and Systems (AIMS) CDT, University of Oxford:
"Probabilistic Model Checking and Strategy Synthesis for Robot Navigation".
-
May 2015:
New paper applying multi-objective probabilistic model checking to robot navigation,
to appear in IJCAI 2015.
-
Apr 2015:
Attending Dagstuhl seminar
"Challenges and Trends in Probabilistic Programming".
-
Apr 2015:
New paper on permissive controller synthesis to appear in
LMCS
(extended version of TACAS'14 paper).
-
Oct 2014:
Talk at the University of California, Berkeley
in the DREAMS seminar series
(Design of Robotics and Embedded systems, Analysis, and Modeling Seminars):
"Probabilistic Model Checking and Strategy Synthesis".
-
Oct 2014:
Attending the 2014 Google Summer of Code Reunion event, Mountain View, California.
-
Sep 2014:
I'm giving a keynote talk at FMICS'14 in Florence this week:
"Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance".
Slides here.
-
Aug 2014:
New paper to appear at ATVA'14
on new techniques for verifying Markov decision processes with learning- and heuristic-based approaches.
-
Aug 2014:
Here is a report I co-wrote, published by
the London Mathematical Society
and the Smith Institute,
giving an accessible introduction to quantitative verification.
-
Jul 2014:
Two postdoctoral positions are now available at Birmingham
on the HIERATIC project. See
the advert.
The posts run until 30 Sep 2015.
Applications close 17 Aug 2014.
-
Jul 2014:
Lecture at the MOVEP'14
(Modelling and Verification of Parallel Processes) summer school in Nantes:
"Automated Verification of Probabilistic Real-time Systems".
More resources here.
-
Jun 2014:
New paper to appear at IROS'14
on probabilistic model checking and strategy synthesis for co-safe LTL specifications in robotic systems,
with Bruno Lacerda
and Nick Hawes.
-
May 2014:
Here is our contribution to the
Festschrift
for Prakash Panangaden,
on "Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations".
-
Mar 2014:
I'll be lecturing on probabilistic model checking at
MOVEP'14
(the 11th Summer School on Modelling and Verification of Parallel Processes) in Nantes, this July.
-
Feb 2014:
PRISM has been selected to participate in
the 2014 Google Summer of Code.
Contribute to PRISM and get paid for it!
See here for details if you're interested.
-
Jan 2014:
New paper to appear at TACAS'14
on permissive controller synthesis for stochastic games.
-
Nov 2013:
Welcome to new post-doc
Chunyan Mu,
working on this project.
-
Oct 2013:
Talk at NASA Ames,
Robust Software Engineering group:
"Probabilistic Model Checking and Strategy Synthesis"
-
Oct 2013:
Tech talk at Google, Mountain View, California:
"Quantitative Verification: Correctness, Reliability and Beyond"
-
Oct 2013:
Attending the 2013 Google Summer of Code Mentor Summit, Mountain View, California
-
Oct 2013:
Welcome to new PhD student Nishanthan Kamaleson.
-
Sep 2013:
New paper
on compositional verification techniques for probabilistic systems
to appear in Information and Computation
(extended version of TACAS'10 paper).
-
Aug 2013:
Tutorial on "Verification of Probabilistic Real-time Systems"
at the French Summer School on Real-Time Systems (ETR 2013), Toulouse.
-
Aug 2013:
Postdoctoral position now available at Birmingham on the new project
"Automated Game-Theoretic Verification of Security Systems".
See the advert
and apply here.
Applications close 4 Sep 2013.
-
Jul 2013:
New paper
on abstraction refinement for probabilistic timed programs
to appear in Theoretical Computer Science.
-
Jul 2013:
New overview/tutorial paper
on strategy synthesis for probabilistic systems at ATVA'13.
-
Jun 2013:
Fully funded PhD position
at Birmingham on "Quantitative Verification of Complex Systems",
to start from September 2013 onwards.
See here for details.
-
May 2013:
New paper at CSF'13
on "Probabilistic Point-to-Point Information Leakage".
-
Apr 2013:
PRISM has been selected to participate in
the 2013 Google Summer of Code.
Contribute to PRISM and get paid for it!
Details here.
Send me a mail if you're interested.
-
Feb 2013:
New FMSD paper
on model checking of stochastic multi-player games
(extended version of TACAS'12 paper).
-
Feb 2013:
New paper to appear at
the 2013 Strategic Reasoning workshop
on strategic analysis of user-centric networks.
-
Jan 2013:
New TACAS'13 tool paper on
PRISM-games,
a model checker for stochastic multi-player games.
-
Dec 2012:
Seminar
at Imperial College London:
"Automated Game-theoretic Verification for Probabilistic Systems"
-
Dec 2012
Kick-off meeting for the new HIERATIC project, Birmingham, 6-7 Dec.
-
Nov 2012:
Attending Dagstuhl seminar
"Games and Decisions for Rigorous Systems Engineering"
-
Nov 2012:
VMCAI'13 paper
on SMT-based bisimulation for Markov models
-
Oct 2012:
Postdoctoral position now available at Birmingham
on the new HIERATIC project.
See the advert,
the particulars
and apply here.
Applications close 22 Oct 2012.
-
Sep 2012:
New tutorial paper
on probabilistic timed automata (PTAs)
in Formal Methods in System Design
-
Jul 2012:
Organising SPIN'12 at Oxford, 23-24 July
-
Jul 2012:
ATVA'12 paper
on "Pareto Curves for Probabilistic Model Checking"
-
Jul 2012:
RV'12 paper
on incremental/runtime methods for probabilistic model checking
-
Jun 2012:
Seminar at Birmingham's Centre for Systems Biology (CSB):
"Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking"
-
May 2012:
Departmental seminar
at the University of Liverpool:
"Automatic Verification of Competitive Stochastic Systems"
-
May 2012:
QEST'12 paper
on the new PRISM benchmark suite.
-
Mar 2012:
TACAS'12 paper
on model checking of stochastic multi-player games
(and new tool PRISM-games)
-
Mar 2012:
LFCS seminar
at the University of Edinburgh
-
Dec 2011:
Royal Society Interface paper
on probabilistic model checking of DNA circuits
-
Jul 2011:
CAV'11 tool paper
on the new version of PRISM
Projects
Current research projects:
- Adversarially-robust neural networks for cyber security (NCSC/GCHQ funded, 2019-23)
- FUN2MODEL (ERC-funded, external collaborator, 2019-24)
- PRINCESS
(part of the BRASS program;
DARPA-funded, co-investigator, 2015-19)
Previous research projects:
- HIERATIC (EU-FP7-funded, co-investigator, 2012-16)
- Automated Game-Theoretic Verification of Security Systems (EPSRC-funded, principal investigator, 2013-14)
- VERIWARE (ERC-funded, associate member, 2010-16)
- PRISMATIC (DARPA-funded, co-investigator, 2010-11)
- Automated quantitative software verification with PRISM (EPSRC-funded, named researcher, 2007-10)
- Predictive Modelling of Signalling Pathways via Probabilistic Model Checking with PRISM (MSR-funded, named researcher, 2006-07)
- Automated Verification of Probabilistic Protocols with PRISM (EPSRC-funded, named researcher, 2003-06)
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.
- IJCAI-PRICAI 2020
(Intl. Joint Conference on Artificial Intelligence & Pacific Rim Intl. Conference on Artificial Intelligence)
- QEST 2020
(Intl. Conference on Quantitative Evaluation of SysTems)
- TACAS 2020 [PC co-chair]
(Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
- MARS 2020
(Intl. Workshop on Models for Formal Analysis of Real Systems)
Some previous programme committees:
-
- AAAI 2020
(AAAI Conference on Artificial Intelligence)
- QEST 2019 [PC co-chair]
(Intl. Conference on Quantitative Evaluation of SysTems)
- IJCAI 2019
(Intl. Joint Conference on Artificial Intelligence)
- FT4DAS 2019
(Intl. Workshop on Formal Techniques for Dependable Autonomous Systems)
- TACAS 2019
(Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
- InterAVT 2019
(Interactive Workshop on the Industrial Application of Verification and Testing)
- ICECCS 2018
(Intl. Conference On Engineering Of Complex Computer Systems)
- FORMATS 2018
(Intl. Conference on Formal Modeling and Analysis of Timed Systems)
- TACAS 2018
(Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
- IJCAI 2018
(Intl. Joint Conference on Artificial Intelligence)
- VaVaS 2018
(Intl. Workshop on Verification and Validation of Autonomous Systems)
- 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)
- 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 [PC 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 [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)
- 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