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 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.
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]
-
Sep 2024:
New paper on integrating adaptive conformal prediction into safe POMDP online planning
to appear in IEEE Robotics and Automation Letters (RA-L).
-
Sep 2024:
I'm giving a keynote talk at FACS 2024 (Intl. Conf. on Formal Aspects of Component Software) on
"Verification and Control of Stochastic Multi-agent Systems".
-
Sep 2024:
Attending the
"Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy" Dagstuhl seminar.
-
Jul 2024:
Post-doc opportunity at Oxford. Come and work with us on verified decision making
as part of the UKRI AI Hub Project. Applications close 15 July 2024.
-
Jul 2024:
Three new papers on verifying stochastic games with neural perception mechanisms to appear in
FM 2024,
L4DC 2024 and
Information and Computation.
-
Jun 2024:
Attending the
"Stochastic Games" Dagstuhl seminar
and presenting an invited tutorial on
"PRISM-games: Model Checking for Stochastic Games".
-
Apr 2024:
I'm very honoured to have won the 2024
ETAPS Test-of-Time Tool Award
for PRISM,
jointly with Marta Kwiatkowska
and Gethin Norman.
Many thanks to all the PRISM
contributors
and collaborators.
For more details, see the talk slides
and news item.
-
Mar 2024:
Organising the Dagstuhl meeting
"Towards A Unified Interface For Modern Probabilistic Model Checking Tools".
-
Mar 2024:
New paper proposing a distributional approach to probabilistic model checking
to appear at NFM 2024.
-
Feb 2024:
New paper "Tools at the Frontiers of Quantitative Verification"
presents a survey of the state of the art in quantitative verification tools, for the latest edition of QComp.
-
Feb 2024:
New paper "Safe POMDP Online Planning via Shielding"
to appear at ICRA 2024, on shielding techniques for online POMDP solution.
-
Nov 2023:
PRISM-games 3.2 is now out,
including symbolic model checking of turn-based stochastic games, correlated/fair equilibria and more.
Further information here.
-
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".
-
Jul 2023:
PRISM 4.8 is now available,
including robust verification of uncertain models (interval MDPs, interval DTMCs), improved strategy/policy generation
and more.
-
Jun 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.
-
Feb 2023:
Our paper "Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions"
is now published in JAIR.
-
Oct 2022:
New paper at NeurIPS 2022
on robust anytime learning of Markov decision processes.
-
Sep 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.
-
Sep 2022:
Our TACAS 2020 special issue is now published at STTT
(overview here).
-
Sep 2022:
I have now joined the Department of Computer Science
at the University of Oxford.
-
Jun 2022:
New paper at UAI 2022
on neuro-symbolic concurrent stochastic games.
-
Jun 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).
-
Apr 2022:
New paper at NFM 2022 on verifying probabilistic policies for deep reinforcement learning.
-
Feb 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!
-
Feb 2022:
New ICCPS 2022 paper on multi-objective controller synthesis with uncertain human preferences.
-
Jan 2022:
New paper on correlated equilibria and fairness for concurrent stochastic games to appear at
TACAS 2022.
-
Dec 2021:
New paper on scenario-based controller synthesis for autonomous systems to appear at
AAAI 2022.
-
Dec 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).
-
Nov 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.
-
Nov 2021:
I'll be PC co-chair of FORMATS 2022 with Sergiy Bogomolov,
to be held in Warsaw in September 2022. Submit your papers!
-
Sep 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.
-
Sep 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.
-
Aug 2021:
Congratulations to Fatma Faruq,
who successfully defended her PhD thesis
"Verified Multi-Robot Planning Under Uncertainty" this week.
-
Jul 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:
Previous research projects:
- Adversarially-robust neural networks for cyber security (NCSC/GCHQ funded, 2019-23)
- 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.
- RP 2024
(Intl. Conference on Reachability Problems)
- NeurIPS 2024
(Intl. Conference on Neural Information Processing Systems)
- UAI 2024
(Intl. Conference on Uncertainty in Artificial Intelligence)
- QEST/FORMATS 2024
(Intl. Conference on Quantitative Evaluation of SysTems/Formal Modeling and Analysis of Timed Systems)
- 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)
I am also on the editorial board for:
Some previous programme committees: