Dave Parker

Prof

Accepting PhD Students

PhD projects

David Parker's research focuses on verification: formal techniques for checking that systems function correctly. In particular, he is interested in quantitative verification, which focuses on the analysis of systems with probabilistic and real-time behaviour. Dr Parker's work spans the development of new theory, algorithms and tools for this area, as well as investigating its applicability to a wide range of areas, including biology and security. He also leads the development of the probabilistic model checking tool PRISM.

20012021

Research activity per year

If you made any changes in Pure these will be visible here soon.
Filter
Conference contribution

Search results

  • 2021

    Optimal online dispatch for high-capacity shared autonomous mobility-on-demand systems

    Li, C., Parker, D. & Hao, Q., 18 Oct 2021, 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE, 7 p. (IEEE International Conference on Robotics and Automation (ICRA)).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    55 Downloads (Pure)
  • Sampling-based robust control of autonomous systems with non-Gaussian noise

    Badings, T. S., Abate, A., Jansen, N., Parker, D., Poonawala, H. A. & Stoelinga, M., 1 Dec 2021, (Accepted/In press) AAAI'22 Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence. AAAI Press, (Proceedings of the AAAI Conference on Artificial Intelligence).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    2 Downloads (Pure)
  • Vehicle dispatch in on-demand ride-sharing with stochastic travel times

    Li, C., Parker, D. & Hao, Q., 16 Dec 2021, 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE, p. 5966-5972 (IEEE International Workshop on Intelligent Robots and Systems (IROS)).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    41 Downloads (Pure)
  • Verifying reinforcement learning up to infinity

    Bacci, E., Gia­cob­be, M. & Parker, D., 27 Aug 2021, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence: Montreal, 19-27 August 2021. Zhou, Z-H. (ed.). International Joint Conferences on Artificial Intelligence Organization (IJCAI), p. 2154-2160 7 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    54 Downloads (Pure)
  • 2020

    Multi-player Equilibria Verification for Concurrent Stochastic Games

    Kwiatkowska, M., Norman, G., Parker, D. & Santos, G., 19 Jun 2020, (Accepted/In press) Proceedings of the 17th International Conference on Quantitative Evaluation of SysTems (QEST'20). Springer, 21 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report

    Budde, C. E., Hartmanns, A., Klauck, M., Křetínský, J., Parker, D., Quatmann, T., Turrini, A. & Zhang, Z., 13 Jul 2020, (Accepted/In press) Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'20). Springer, 25 p. (Lecture Notes in Comuter Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time

    Kwiatkowska, M., Norman, G., Parker, D. & Santos, G., 6 Apr 2020, (Accepted/In press) 32nd International Conference on Computer Aided Verification (CAV 2020), Proceedings. Springer, 12 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Probabilistic Guarantees for Safe Deep Reinforcement Learning

    Bacci, E. & Parker, D., 29 Jun 2020, (Accepted/In press) Proceedings of 18th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2020). Bertrand, N. & Jansen, N. (eds.). Springer, 18 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Quantitative Verification of Certificate Transparency Gossip Protocols

    Oxford, M., Parker, D. & Ryan, M., 3 May 2020, (Accepted/In press) Proceedings of 6th International Workshop on Security and Privacy in the Cloud (SPC'20). IEEE Computer Society Press, 9 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2019

    Automated formal analysis of side-channel attacks on probabilistic systems

    Novakovic, C. & Parker, D., 15 Sep 2019, Computer Security – ESORICS 2019: 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I. Sako, K., Schneider, S. & Ryan, P. Y. A. (eds.). Springer, p. 319-337 19 p. (Lecture Notes in Computer Science ; vol. 11735)(Security and Cryptology; vol. 11735).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    155 Downloads (Pure)
  • Equilibria-based probabilistic model checking for concurrent stochastic games

    Kwiatkowska, M., Norman, G., Parker, D. & Santos, G., 23 Sep 2019, Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. ter Beek, M. H., McIver, A. & Oliveira, J. N. (eds.). Springer, p. 298-315 18 p. (Lecture Notes in Computer Science; vol. 11800)(Programming and Software Engineering; vol. 11800).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    3 Citations (Scopus)
    156 Downloads (Pure)
  • Quantitative verification of numerical stability for Kalman filters

    Evangelidis, A. & Parker, D., 23 Sep 2019, Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. Springer, 17 p. (Lecture Notes in Computer Science; vol. 11800).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    2 Citations (Scopus)
    147 Downloads (Pure)
  • Simultaneous task allocation and planning under uncertainty

    Faruq, F., Lacerda, B., Hawes, N. & Parker, D., 7 Jan 2019, 2018 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE Computer Society Press, p. 3559-3564 6 p. (IEEE International Workshop on Intelligent Robots and Systems (IROS) ).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    9 Citations (Scopus)
    203 Downloads (Pure)
  • The 2019 comparison of tools for the analysis of quantitative formal models (QComp 2019 competition report)

    Hahn, E. M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kretínský, J., Parker, D., Quatmann, T., Ruijters, E. & Steinmetz, M., 4 Apr 2019, (E-pub ahead of print) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2019. Beyer, D., Huisman, M., Kordon, F. & Steffen, B. (eds.). Springer, Vol. 3. p. 69-92 24 p. (Lecture Notes in Computer Science; vol. 11429).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    17 Citations (Scopus)
    251 Downloads (Pure)
  • The quantitative verification benchmark set

    Hartmanns, A., Klauck, M., Parker, D., Quatmann, T. & Ruijters, E., 4 Apr 2019, (E-pub ahead of print) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2019. Beyer, D., Huisman, M., Kordon, F. & Steffen, B. (eds.). Springer, Vol. 1. p. 344–350 7 p. (Lecture Notes in Computer Science; vol. 11427).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    10 Citations (Scopus)
    126 Downloads (Pure)
  • Verification and control of turn-based probabilistic real-time games

    Kwiatkowska, M., Norman, G. & Parker, D., 4 Nov 2019, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday. Alvim, M., Chatzikokolakis, K., Olarte, C. & Valencia, F. (eds.). Springer, Vol. 11760. p. 379-396 16 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    3 Citations (Scopus)
    98 Downloads (Pure)
  • 2018

    Automated Verification of Concurrent Stochastic Games

    Kwiatkowska, M., Norman, G., Parker, D. & Santos, G., 15 Aug 2018, Proceedings of the 15th International Conference on Quantitative Evaluation of SysTems (QEST'18).. Springer, 16 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    7 Citations (Scopus)
    141 Downloads (Pure)
  • Online fault diagnosis in Petri net models of discrete-event systems using Fourier-Motzkin

    Al-Ajeli, A. & Parker, D., 1 Nov 2018, Proceedings of the 12th UKACC International Conference on Control. IEEE Xplore, p. 397-402 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    1 Citation (Scopus)
    149 Downloads (Pure)
  • 2017

    Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes

    Baier, C., Klein, J., Leuschner, L. & Parker, D., Jul 2017, Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings. Majumdar, R. & Kunčak, V. (eds.). Springer, p. 160-180 21 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    21 Citations (Scopus)
    196 Downloads (Pure)
  • Multi-objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees

    Lacerda, B., Parker, D. & Hawes, N., 26 Jan 2017, (Accepted/In press) Proceedings of the twenty seventh International Conference on Automated Planning and Scheduling (ICAPS 2017). AAAI Press, 9 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Performance Modelling and Verification of Cloud-based Auto-Scaling Policies

    Evangelidis, A., Parker, D. & Bahsoon, R., 13 Jul 2017, Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. IEEE Computer Society Press, p. 355 364 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Performance Modelling and Verification of Cloud-based Auto-Scaling Policies

    Evangelidis, A., Parker, D. & Bahsoon, R., 13 Jul 2017, Proceedings of 2017 IEEE/ACM 17th International Symposium on Cluster, Cloud and Grid Computing (CCGrid'17). IEEE Xplore, p. 355-364

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    10 Citations (Scopus)
    256 Downloads (Pure)
  • Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata

    Kwiatkowska, M., Norman, G. & Parker, D., 25 Jul 2017, KiMfest : A conference in honour of Kim G. Larsen on the occasion of his 60th birthday. Springer, p. 289-309 21 p. (Lecture Notes in Computer Science ; vol. 10460).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    125 Downloads (Pure)
  • 2016

    Finite-Horizon Bisimulation Minimisation for Probabilistic Systems

    Kamaleson, N., Parker, D. & Rowe, J., 8 Apr 2016, Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer, p. 147-164 18 p. (Lecture Notes in Computer Science; vol. 9641).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    2 Citations (Scopus)
    155 Downloads (Pure)
  • Formal Quantitative Analysis of Reaction Networks Using Chemical Organisation Theory

    Mu, C., Dittrich, P., Parker, D. & Rowe, J., 2016, Computational Methods in Systems Biology: 14th International Conference, CMSB 2016, Cambridge, UK, September 21-23, 2016, Proceedings. Springer, p. 232-251 (Lecture Notes in Computer Science; vol. 9859).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    12 Citations (Scopus)
    153 Downloads (Pure)
  • PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games

    Kwiatkowska, M., Parker, D. & Wiltsche, C., 9 Apr 2016, Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16). Chechik, M. & Raskin, J-F. (eds.). Springer, 6 p. (Lecture Notes in Computer Science; vol. 9636).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    22 Citations (Scopus)
    173 Downloads (Pure)
  • Quantitative Verification and Synthesis of Attack-Defence Scenarios

    Aslanyan, Z., Nielson, F. & Parker, D., 11 Aug 2016, (E-pub ahead of print) Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16). IEEE Xplore

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
    41 Citations (Scopus)
    189 Downloads (Pure)
  • 2015

    Nested value iteration for partially satisfiable co-safe ltl specifications (Extended Abstract)

    Lacerda, B., Parker, D. & Hawes, N., 2015, AAAI Fall Symposium - Technical Report. AI Access Foundation, Vol. FS-15-06. p. 54-55 2 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    2 Citations (Scopus)
  • Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications

    Lacerda, B., Parker, D. & Hawes, N., 20 Jul 2015, Proc. 24th International Joint Conference on Artificial Intelligence (IJCAI'15). Yang, Q. & Wooldridge, M. (eds.). Association for the Advancement of Artificial Intelligence, p. 1587-1593

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    24 Citations (Scopus)
    9 Downloads (Pure)
  • 2014

    An investigation into the feasibility of radioactive gas imaging for studies in process tomography

    Bell, S. D., Ingram, A., Leadbeater, T. W. & Parker, D. J., 1 Jan 2014, 7th World Congress in Industrial Process Tomography. International Society for Industrial Process Tomography, p. 897-906 10 p. (7th World Congress in Industrial Process Tomography).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Optimal and dynamic planning for Markov decision processes with co-safe LTL specifications

    Lacerda, B., Parker, D. & Hawes, N., 31 Oct 2014, IEEE International Conference on Intelligent Robots and Systems. Institute of Electrical and Electronics Engineers (IEEE), p. 1511-1516 6 p. 6942756

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    35 Citations (Scopus)
  • Probabilistic model checking of labelled markov processes via finite approximate bisimulations

    Abate, A., Kwiatkowska, M., Norman, G. & Parker, D., 2014, Horizons of the Mind. A Tribute to Prakash Panangaden : Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday. van Breugel, F., Kashefi, E., Palamidessi, C. & Rutten, J. (eds.). Springer, Vol. 8464 LNCS. p. 40-58 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8464 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    14 Citations (Scopus)
  • Verification of markov decision processes using learning algorithms

    Brázdil, T., Chatterjee, K., Chmelík, M., Forejt, V., Křetínský, J., Kwiatkowska, M., Parker, D. & Ujma, M., 2014, Automated Technology for Verification and Analysis : 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings. Cassez, F. & Raskin, J-F. (eds.). Springer, Vol. 8837. p. 98-114 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8837).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    81 Citations (Scopus)
  • 2013

    Probabilistic point-to-point information leakage

    Chothia, T., Kawamoto, Y., Novakovic, C. & Parker, D., 9 Oct 2013, Proceedings - 2013 IEEE 26th Computer Security Foundations Symposium, CSF 2013. p. 193-205 13 p. 6595829

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    20 Citations (Scopus)
  • 2012

    The PRISM benchmark suite

    Kwiatkowsa, M., Norman, G. & Parker, D., 2012, Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST'12).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2010

    Assume-Guarantee Verification for Probabilistic Systems

    Kwiatkowska, M., Norman, G., Parker, D. & Qu, H., 2010, Tools and Algorithms for the Construction and Analysis of Systems : 6th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Esparza, J. & Majumdar, R. (eds.). Springer, p. 23-37 (Lecture Notes in Computer Science; vol. 6015).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    85 Citations (Scopus)
  • 2007

    Stochastic model checking

    Kwiatkowska, M., Norman, G. & Parker, D., 2007, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution