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.

20012022

Research activity per year

Filter
Conference contribution

Search results

  • Conference contribution

    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

  • 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)
  • Automated formal analysis of side-channel attacks on probabilistic systems

    Novakovic, C. & Parker, D., 15 Sept 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
    199 Downloads (Pure)
  • 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)
    200 Downloads (Pure)
  • A value-based dynamic learning approach for vehicle dispatch in ride-sharing

    Li, C., Parker, D. & Hao, Q., 26 Dec 2022, (E-pub ahead of print) 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2022). IEEE, p. 11388-11395 8 p. (IEEE/RSJ International Conference on Intelligent Robots and Systems).

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

    Open Access
    File
    30 Downloads (Pure)
  • Correlated equilibria and fairness in concurrent stochastic games

    Kwiatkowska, M., Norman, G., Parker, D. & Santos, G., 30 Mar 2022, TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems. Fisman, D. & Rosu, G. (eds.). Springer, p. 60–78 (Lecture Notes in Computer Science; no. 13244).

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

    Open Access
    File
    26 Downloads (Pure)
  • 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)
    276 Downloads (Pure)
  • Equilibria-based probabilistic model checking for concurrent stochastic games

    Kwiatkowska, M., Norman, G., Parker, D. & Santos, G., 23 Sept 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)
    236 Downloads (Pure)
  • 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)
    230 Downloads (Pure)
  • Finite-horizon equilibria for neuro-symbolic concurrent stochastic games

    Yan, R., Santos, G., Duan, X., Parker, D. & Kwiatkowska, M., 28 Sept 2022, Proceedings of the 38th Conference on Uncertainty in Artificial Intelligence: Uncertainty in Artificial Intelligence, 1-5 August 2022, Eindhoven, The Netherlands. Cussens, J. & Zhang, K. (eds.). Proceedings of Machine Learning Research, p. 2170-2180 11 p. (Proceedings of Machine Learning Research; vol. 180).

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

    Open Access
    File
    18 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)
    231 Downloads (Pure)
  • Multi-objective controller synthesis with uncertain human preferences

    Chen, S., Boggess, K., Parker, D. & Feng, L., 24 Jun 2022, (E-pub ahead of print) 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS). Los Alamitos, California, Washington, Tokyo: IEEE, Vol. 2022. p. 170-180 11 p. (ACM/IEEE International Conference on Cyber-Physical Systems).

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

    Open Access
    File
    8 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

  • 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

  • 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)
  • 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

    Open Access
    File
    23 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)
    206 Downloads (Pure)
  • 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)
  • 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
    170 Downloads (Pure)
  • 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)
  • 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)
    351 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)
    234 Downloads (Pure)
  • 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

  • Probabilistic model checking for strategic equilibria-based decision making: advances and challenges

    Kwiatkowska, M., Norman, G., Parker, D., Santos, G. & Yan, R., 22 Aug 2022, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Szeider, S., Ganian, R. & Silva, A. (eds.). Dagstuhl, Germany: Schloss Dagstuhl, Vol. 241. 22 p. 4. (Leibniz International Proceedings in Informatics).

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

    Open Access
    File
    31 Downloads (Pure)
  • 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)
  • 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)
  • 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)
    263 Downloads (Pure)
  • 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

  • Quantitative verification of numerical stability for Kalman filters

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

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

    Open Access
    File
    2 Citations (Scopus)
    201 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., 28 Jun 2022, Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence. Palo Alto, California: AAAI Press, p. 9669-9678 11 p. (Proceedings of the AAAI Conference on Artificial Intelligence; vol. 36, no. 9).

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

    Open Access
    File
    28 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)
    297 Downloads (Pure)
  • 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

  • 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
    186 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)
    342 Downloads (Pure)
  • 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

  • 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)
    228 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 (Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems).

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

    Open Access
    File
    172 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)
    149 Downloads (Pure)
  • 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)
  • Verified probabilistic policies for deep reinforcement learning

    Bacci, E. & Parker, D., 20 May 2022, NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. Deshmukh, J. V., Havelund, K. & Perez, I. (eds.). Cham: Springer, Vol. 13260. p. 193-212 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13260 LNCS).

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

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

    Bacci, E., Giacobbe, 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
    192 Downloads (Pure)