David Parker
Professor of Computer Science, University of Oxford
|
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 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 formal models of systems with probabilistic and real-time behaviour.
I work on a wide range of topics within probabilistic verification spanning theory and practice.
I am currently particularly interested in game-theoretic methods for verification and controller synthesis,
and formal verification of AI-driven systems such as robotics and autonomous systems.
I'm also interested in the application of verification to computer security.
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 2023:
Welcome to new PhD student Yannik Schnitzer.
-
Sep 2023:
I'm giving a keynote talk at QEST /
CONFEST 2023
on "Multi-Agent Verification and Control with Probabilistic Model Checking".
There is an accompanying paper here.
-
May 2023:
I'm lecturing at the European Summer School on Artificial Intelligence (ESSAI) this week,
with Nick Hawes and Bruno Lacerda.
Course material is here:
"Model Uncertainty in Sequential Decision Making".
-
July 2023:
PRISM 4.8 is now available,
including robust verification of uncertain models (interval MDPs, interval DTMCs), improved strategy/policy generation
and more.
-
June 2023:
Attending Dagstuhl seminar
"Scalable Analysis of Probabilistic Models and Programs".
-
May 2023:
I'll be giving a tutorial at the European Summer School on Artificial Intelligence (ESSAI)
on "Model Uncertainty in Sequential Decision Making""
with Nick Hawes and Bruno Lacerda.
-
February 2023:
Our paper "Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions"
is now published in JAIR.
-
October 2022:
New paper at NeurIPS 2022
on robust anytime learning of Markov decision processes.
-
September 2022:
Organising FORMATS 2022 this week
with Sergiy Bogomolov
as part of CONFEST 2022.
We have a great programe.
Hope to see you in Warsaw.
-
September 2022:
Our TACAS 2020 special issue is now published at STTT
(overview here).
-
September 2022:
I have now joined the Department of Computer Science
at the University of Oxford.
-
June 2022:
New paper at UAI 2022
on neuro-symbolic concurrent stochastic games.
-
June 2022:
I'm delighted to join the editorial board for
Formal Aspects of Computing.
-
May 2022:
Congratulations to Cheng Li,
who successfully defended his PhD thesis
"Vehicle Dispatch in High-Capacity Shared Autonomous Mobility-On-Demand Systems" this week
(see papers in ICRA'21,
IROS'21 and IROS'22).
-
April 2022:
New paper at NFM 2022 on verifying probabilistic policies for deep reinforcement learning.
-
February 2022:
AAAI 2022 distinguished paper award (one of just 6)
for Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise.
Congratulations especially to Thom!
-
February 2022:
New ICCPS 2022 paper on multi-objective controller synthesis with uncertain human preferences.
-
January 2022:
New paper on correlated equilibria and fairness for concurrent stochastic games to appear at
TACAS 2022.
-
December 2021:
New paper on scenario-based controller synthesis for autonomous systems to appear at
AAAI 2022.
-
December 2021:
Congratulations to Edoardo Bacci,
who successfully defended his PhD thesis
"Formal Verification of Deep Reinforcement Learning Agents" this week
(see papers in FORMATS'20,
IJCAI'21 and
NFM'22).
-
November 2021:
New survey paper Probabilistic Model Checking and Autonomy to appear in Annual Review of Control, Robotics, and Autonomous Systems next year, covering MDPs, POMDPs and stochastic games.
-
November 2021:
I'll be PC co-chair of FORMATS 2022 with Sergiy Bogomolov,
to be held in Warsaw in September 2022. Submit your papers!
-
September 2021:
PRISM is 20 years old this month!
It's first official release was in 2001.
Thanks to all those have
used it and who have helped
develop it over the years.
-
September 2021:
I'm happy to announce that I'll be a
Turing Fellow
at the Alan Turing Institute
from October 2021, working on formal verification of AI systems.
-
August 2021:
Congratulations to Fatma Faruq,
who successfully defended her PhD thesis
"Verified Multi-Robot Planning Under Uncertainty" this week.
-
July 2021:
I am giving an invited tutorial at
EXPRESS/SOS 2021 next month
on "Probabilistic Verification of Concurrent Autonomous Systems".
-
May 2021:
New paper on time-unbounded verification of reinforcement learning to appear at
IJCAI 2021.
-
May 2021:
Congratulations to Michael Oxford,
who successfully defended his PhD thesis
"Quantitative Verification of Gossip Protocols for Certificate Transparency" this week.
-
Mar 2021:
PRISM 4.7 is now available,
including support for POMDPs, improved accuracy reporting
and more.
-
Jan 2021:
There are now over 400 papers by external research teams using or building on PRISM.
-
Jan 2021:
Congratulations to Irfan Muhammad, who successfully defended his PhD thesis
"Algorithms for Reachability Problems on Stochastic Markov Reward Models" this week.
-
Dec 2020:
New paper to appear in
Formal Methods in System Design
covering our recent thread of work on
on verifying concurrent stochastic games,
as implemented in PRISM-games.
-
Nov 2020:
I'll be giving a keynote at iFM 2020,
(International Conference on integrated Formal Methods)
on "Verification with Stochastic Games: Advances and Challenges".
-
Jul 2020:
New paper on probabilistic guarantees for deep reinforcement learning to appear at
FORMATS 2020.
-
Jul 2020:
New paper on verifying multi-coalition equilibria for concurrent stochastic games to appear at
QEST 2020.
-
May 2020:
New paper at
CAV 2020
describing version 3.0 of PRISM-games,
featuring concurrent stochastic games, equilibria, real-time models
and many new examples.
-
May 2020:
Congratulations to Alexandros Evangelidis,
who successfully defended his PhD thesis
"Verified Control and Estimation for Cloud Computing" this week
(see papers in CCGrid'17,
FGCS
and FM'19).
-
Apr 2019:
The papers for TACAS 2020
are now online.
Sadly, ETAPS could not happen as planned in April,
but the papers are all open access and available.
-
Jan 2020:
PRISM-games version 3.0 is now available,
providing concurrent stochastic games,
equilibria, real-time models
and many new examples.
More information here.
-
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.
-
Jul 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:
- FUN2MODEL (ERC-funded, external collaborator, 2019-24)
- Adversarially-robust neural networks for cyber security (NCSC/GCHQ funded, 2019-23)
Previous research projects:
- Aion (VeTTS-funded, with Vincent Rahli, 2020-21)
- PRINCESS
(part of the BRASS program;
DARPA-funded, co-investigator, 2015-19)
- 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.
- AAAI 2024
(AAAI Conference on Artificial Intelligence)
- MARS 2024
(Intl. Workshop on Models for Formal Analysis of Real Systems)
- MOVEP 2024
(Intl. Summer School on Modelling and Verification of Parallel Processes)
- SETTA 2023
(Intl. Symposium on Dependable Software Engineering)
- QEST 2023
(Intl. Conference on Quantitative Evaluation of SysTems)
I am also on the editorial board for
Formal Aspects of Computing.
Some previous programme committees: