David Parker

Lecturer
School of Computer Science
University of Birmingham
Edgbaston, Birmingham, B15 2TT

Email: d.a.parker@cs.bham.ac.uk
Tel: +44 (0) 121 41 47264
Office: 107
Office hours: Wed 12.30-1.30, Thu 3-4

<< NEWS >>

Postdoc position at Birmingham on "Automated Game-Theoretic Verification of Security Systems". Applications close 4 Sep 2013.

I'm a 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, focusing on the analysis of systems 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 systems biology, DNA computing and computer security.

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

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.

For more details about my research, see here.

News & Activities [+]

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

Publications

See my online list of papers or my pages on DBLP, Google Scholar or Scopus.

Projects

Current research projects:

Automated Game-Theoretic Verification of Security Systems (EPSRC-funded, principal investigator, to commence)
HIERATIC (EU-FP7-funded, co-investigator, 2012-15)
VERIWARE (ERC-funded, associate member, 2010-15)

Previous research projects:

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)

People

PhD students:

Nishanthan Kamaleson (2013-, co-supervised with Jon Rowe)
Mateusz Ujma (2011-, co-supervised with Marta Kwiatkowska)

Post-docs:

Marius Bujorianu (2012-, with Jon Rowe on HIERATIC)

Events

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

QAPL 2014 (Intl. Workshop on Quantitative Aspects of Programming Languages)
SIMUTools 2014 (Intl. Conference on Simulation Tools and Techniques)
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)

Previous programme committees:

- 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
- PASM 2005
- PASM 2004

Talks & Tutorials

Here are slides from some recent talks and tutorials.

Teaching & Student Projects

Current teaching and administration:

Lecturing "Information & the Web", Spring Term 2012-13
Course director and admissions for the MSc in Advanced Computer Science
MSc mini-projects and advanced projects

I am happy to supervise final year or MSc student projects.

Between 2008-2012, I taught a lecture course on Probabilistic Model Checking at Oxford. I maintain up-to-date copies of the lecture material here.