Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation. - Luca de Alfaro; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Roberto Segala (TACAS, 2000)

Faster and Symbolic CTMC Model Checking. - Joost-Pieter Katoen; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (PAPM-PROBMIV, 2001)

PRISM: Probabilistic Symbolic Model Checker. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Computer Performance Evaluation / TOOLS, 2002)

Computer Based Real-Time Simulator for Renewable Energy Converters. - David Parker 001 (DELTA, 2002)

Formal analysis and validation of continuous-time Markov chain based system level power management strategies. - Gethin Norman; David Parker 001; Marta Z. Kwiatkowska; Sandeep K. Shukla; Rajesh K. Gupta 001 (HLDVT, 2002)

A Symbolic Out-of-Core Solution Method for Markov Models. - Marta Z. Kwiatkowska; Rashid Mehmood; Gethin Norman; David Parker 001 (PDMC@CONCUR, 2002)

On the use of MTBDDs for performability analysis and verification of stochastic systems. - Holger Hermanns; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Markus Siegle (J. Log. Algebraic Methods Program., 2003)

Implementation of symbolic model checking for probabilistic systems. - David Anthony Parker (2003)

Mathematical techniques for analyzing concurrent and probabilistic systems. - Jan J. M. M. Rutten; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Prakash Panangaden (American Mathematical Society, 2004)

Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking. - Marta Z. Kwiatkowska; David Parker 001; Yi Zhang; Rashid Mehmood (MASCOTS, 2004)

PRISM 2.0: A Tool for Probabilistic Model Checking. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (QEST, 2004)

Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. - Håkan L. S. Younes; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (TACAS, 2004)

Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking. - Gethin Norman; David Parker 001; Marta Z. Kwiatkowska; Sandeep K. Shukla (VLSI Design, 2004)

Symbolic Representations and Analysis of Large Probabilistic Systems. - Andrew S. Miner; David Parker 001 (Validation of Stochastic Systems, 2004)

Probabilistic symbolic model checking with PRISM: a hybrid approach. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Int. J. Softw. Tools Technol. Transf., 2004)

A Wavefront Parallelisation of CTMC Solution Using MTBDDs. - Yi Zhang; David Parker 001; Marta Z. Kwiatkowska (DSN, 2005)

Quantitative Analysis With the Probabilistic Model Checker PRISM. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (QAPL, 2005)

Using probabilistic model checking for dynamic power management. - Gethin Norman; David Parker 001; Marta Z. Kwiatkowska; Sandeep K. Shukla; Rajesh Gupta 001 (Formal Aspects Comput., 2005)

Probabilistic model checking in practice: case studies with PRISM. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SIGMETRICS Perform. Evaluation Rev., 2005)

Evaluating the reliability of NAND multiplexing with PRISM. - Gethin Norman; David Parker 001; Marta Z. Kwiatkowska; Sandeep K. Shukla (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2005)

Symmetry Reduction for Probabilistic Model Checking. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (CAV, 2006)

On Reduction Criteria for Probabilistic Reward Models. - Marcus Größer; Gethin Norman; Christel Baier; Frank Ciesinski; Marta Z. Kwiatkowska; David Parker 001 (FSTTCS, 2006)

Game-based Abstraction for Markov Decision Processes. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (QEST, 2006)

PRISM: A Tool for Automatic Verification of Probabilistic Systems. - Andrew Hinton; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (TACAS, 2006)

Simulation and verification for computational modelling of signalling pathways. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Oksana Tymchyshyn; John Heath; Eamonn A. Gaffney (WSC, 2006)

Performance analysis of probabilistic timed automata using digital clocks. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Jeremy Sproston (Formal Methods Syst. Des., 2006)

A formal analysis of bluetooth device discovery. - Marie Duflot; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Int. J. Softw. Tools Technol. Transf., 2006)

Numerical vs. statistical probabilistic model checking. - Håkan L. S. Younes; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Int. J. Softw. Tools Technol. Transf., 2006)

GRIP: Generic Representatives in PRISM. - Alastair F. Donaldson; Alice Miller 001; David Parker 001 (QEST, 2007)

Model checking the probabilistic pi-calculus. - Gethin Norman; Catuscia Palamidessi; David Parker 001; Peng Wu 002 (QEST, 2007)

Stochastic Model Checking. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SFM, 2007)

Symbolic Magnifying Lens Abstraction in Markov Decision Processes. - Pritam Roy; David Parker 001; Gethin Norman; Luca de Alfaro (QEST, 2008)

Generating Compact MTBDD-Representations from ProbmelaSpecifications. - Frank Ciesinski; Christel Baier; Marcus Größer; David Parker 001 (SPIN, 2008)

Game-Based Probabilistic Predicate Abstraction in PRISM. - Mark Kattenbelt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (QAPL, 2008)

Using probabilistic model checking in systems biology. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SIGMETRICS Perform. Evaluation Rev., 2008)

Analysis of a gossip protocol in PRISM. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SIGMETRICS Perform. Evaluation Rev., 2008)

Probabilistic model checking of complex biological pathways. - John Heath; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Oksana Tymchyshyn (Theor. Comput. Sci., 2008)

Quantitative Verification Techniques for Biological Processes. - Marta Kwiatkowska; Gethin Norman; David Parker 001 (Algorithmic Bioprocesses, 2009)

Stochastic Games for Verification of Probabilistic Timed Automata. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (FORMATS, 2009)

Bisimulation for Demonic Schedulers. - Konstantinos Chatzikokolakis 001; Gethin Norman; David Parker 001 (FoSSaCS, 2009)

Language-Level Symmetry Reduction for Probabilistic Model Checking. - Alastair F. Donaldson; Alice Miller 001; David Parker 001 (QEST, 2009)

Abstraction Refinement for Probabilistic Software. - Mark Kattenbelt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (VMCAI, 2009)

PRISM: probabilistic model checking for performance and reliability analysis. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SIGMETRICS Perform. Evaluation Rev., 2009)

Probabilistic Mobile Ambients. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Maria Grazia Vigliotti (Theor. Comput. Sci., 2009)

Model Checking Probabilistic and Stochastic Extensions of the pi-Calculus. - Gethin Norman; Catuscia Palamidessi; David Parker 001; Peng Wu 002 (IEEE Trans. Software Eng., 2009)

Advances and challenges of probabilistic model checking. - Marta Kwiatkowska; Gethin Norman; David Parker 001 (Allerton, 2010)

A Framework for Verification of Software with Time and Probabilities. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (FORMATS, 2010)

Compositional Verification of Probabilistic Systems Using Learning. - Lu Feng 001; Marta Z. Kwiatkowska; David Parker 001 (QEST, 2010)

Assume-Guarantee Verification for Probabilistic Systems. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (TACAS, 2010)

A game-based abstraction-refinement framework for Markov decision processes. - Mark Kattenbelt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Formal Methods Syst. Des., 2010)

Learning-Based Compositional Verification for Synchronous Probabilistic Systems. - Lu Feng 001; Tingting Han 001; Marta Z. Kwiatkowska; David Parker 001 (ATVA, 2011)

A Systematic Approach to Evaluate Sustained Stochastic Oscillations. - Jorge Júlvez; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (BICoB, 2011)

PRISM 4.0: Verification of Probabilistic Real-Time Systems. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (CAV, 2011)

Verifying Team Formation Protocols with Probabilistic Model Checking. - Taolue Chen 001; Marta Z. Kwiatkowska; David Parker 001; Aistis Simaitis (CLIMA, 2011)

Incremental quantitative verification for Markov decision processes. - Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001 (DSN, 2011)

Automated Learning of Probabilistic Assumptions for Compositional Reasoning. - Lu Feng 001; Marta Z. Kwiatkowska; David Parker 001 (FASE, 2011)

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. - Ernst Moritz Hahn; Gethin Norman; David Parker 001; Björn Wachter; Lijun Zhang 001 (QEST, 2011)

Automated Verification Techniques for Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (SFM, 2011)

Quantitative Multi-objective Verification for Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (TACAS, 2011)

Pareto Curves for Probabilistic Model Checking. - Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001 (ATVA, 2012)

The PRISM Benchmark Suite. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (QEST, 2012)

Incremental Runtime Verification of Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001; Mateusz Ujma (RV, 2012)

Probabilistic verification of Herman's self-stabilisation algorithm. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Formal Aspects Comput., 2012)

Evaluation of Sustained Stochastic Oscillations by Means of a System of Differential Equations. - Jorge Júlvez; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Int. J. Comput. Their Appl., 2012)

Advances in Probabilistic Model Checking. - Marta Z. Kwiatkowska; David Parker 001 (Software Safety and Security, 2012)

Automated Verification and Strategy Synthesis for Probabilistic Systems. - Marta Z. Kwiatkowska; David Parker 001 (ATVA, 2013)

Probabilistic Point-to-Point Information Leakage. - Tom Chothia; Yusuke Kawamoto 001; Chris Novakovic; David Parker 001 (CSF, 2013)

PRISM-games: A Model Checker for Stochastic Multi-Player Games. - Taolue Chen 001; Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Aistis Simaitis (TACAS, 2013)

SMT-Based Bisimulation Minimisation of Markov Models. - Christian Dehnert; Joost-Pieter Katoen; David Parker 001 (VMCAI, 2013)

Strategic Analysis of Trust Models for User-Centric Networks - Marta Z. Kwiatkowska; David Parker 001; Aistis Simaitis (SR, 2013)

Automatic verification of competitive stochastic systems. - Taolue Chen 001; Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Aistis Simaitis (Formal Methods Syst. Des., 2013)

Model checking for probabilistic timed automata. - Gethin Norman; David Parker 001; Jeremy Sproston (Formal Methods Syst. Des., 2013)

Compositional probabilistic verification through multi-objective model checking. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (Inf. Comput., 2013)

Verification of Markov Decision Processes Using Learning Algorithms. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Vojtech Forejt; Jan Kretínský; Marta Z. Kwiatkowska; David Parker 001; Mateusz Ujma (ATVA, 2014)

Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations. - Alessandro Abate; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001 (Horizons of the Mind, 2014)

On Incremental Quantitative Verification for Probabilistic Systems. - Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001; Mateusz Ujma (HOWARD-60, 2014)

Optimal and dynamic planning for Markov decision processes with co-safe LTL specifications. - Bruno Lacerda; David Parker 001; Nick Hawes (IROS, 2014)

Local abstraction refinement for probabilistic timed programs. - Klaus Dräger; Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001 (Theor. Comput. Sci., 2014)

Nested Value Iteration for Partially Satisfiable Co-Safe LTL Specifications (Extended Abstract). - Bruno Lacerda; David Parker 001; Nick Hawes (AAAI Fall Symposia, 2015)

The Hanoi Omega-Automata Format. - Tomás Babiak; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; Jan Kretínský; David Müller 001; David Parker 001; Jan Strejcek (CAV (1), 2015)

Verification and Control of Partially Observable Probabilistic Real-Time Systems. - Gethin Norman; David Parker 001; Xueyi Zou (FORMATS, 2015)

Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications. - Bruno Lacerda; David Parker 001; Nick Hawes (IJCAI, 2015)

Permissive Controller Synthesis for Probabilistic Systems. - Klaus Dräger; Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Mateusz Ujma (Log. Methods Comput. Sci., 2015)

Formal Quantitative Analysis of Reaction Networks Using Chemical Organisation Theory. - Chunyan Mu; Peter Dittrich; David Parker 001; Jonathan E. Rowe (CMSB, 2016)

Quantitative Verification and Synthesis of Attack-Defence Scenarios. - Zaruhi Aslanyan; Flemming Nielson; David Parker 001 (CSF, 2016)

Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. - Nishanthan Kamaleson; David Parker 001; Jonathan E. Rowe (SPIN, 2016)

PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games. - Marta Kwiatkowska; David Parker 001; Clemens Wiltsche (TACAS, 2016)

Synthesizing efficient systems in probabilistic environments. - Christian von Essen; Barbara Jobstmann; David Parker 001; Rahul Varshneya (Acta Informatica, 2016)

Multi-Objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees. - Bruno Lacerda; David Parker 001; Nick Hawes (ICAPS, 2017)

Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. - Marta Kwiatkowska; Gethin Norman; David Parker 001 (Models, Algorithms, Logics and Tools, 2017)

Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. - Christel Baier; Joachim Klein 001; Linda Leuschner; David Parker 001; Sascha Wunderlich (CAV (1), 2017)

Verification and control of partially observable probabilistic systems. - Gethin Norman; David Parker 001; Xueyi Zou (Real Time Syst., 2017)

Simultaneous Task Allocation and Planning Under Uncertainty. - Fatma Faruq; David Parker 001; Bruno Lacerda; Nick Hawes (IROS, 2018)

Automated Verification of Concurrent Stochastic Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (QEST, 2018)

Performance modelling and verification of cloud-based auto-scaling policies. - Alexandros Evangelidis; David Parker 001; Rami Bahsoon (Future Gener. Comput. Syst., 2018)

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. - Marta Kwiatkowska; David Parker 001; Clemens Wiltsche (Int. J. Softw. Tools Technol. Transf., 2018)

Organisation-Oriented Coarse Graining and Refinement of Stochastic Reaction Networks. - Chunyan Mu; Peter Dittrich; David Parker 001; Jonathan E. Rowe (IEEE ACM Trans. Comput. Biol. Bioinform., 2018)

Replicated Computational Results (RCR) Report for "ProPPA: Probabilistic Programming for Stochastic Dynamical Systems". - David Parker 001 (ACM Trans. Model. Comput. Simul., 2018)

Verification and Control of Turn-Based Probabilistic Real-Time Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001 (The Art of Modelling Computational Systems, 2019)

Automated Formal Analysis of Side-Channel Attacks on Probabilistic Systems. - Chris Novakovic; David Parker 001 (ESORICS (1), 2019)

Quantitative Verification of Numerical Stability for Kalman Filters. - Alexandros Evangelidis; David Parker 001 (FM, 2019)

Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (FM, 2019)

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). - Ernst Moritz Hahn; Arnd Hartmanns; Christian Hensel; Michaela Klauck; Joachim Klein 001; Jan Kretínský; David Parker 001; Tim Quatmann; Enno Ruijters; Marcel Steinmetz (TACAS (3), 2019)

The Quantitative Verification Benchmark Set. - Arnd Hartmanns; Michaela Klauck; David Parker 001; Tim Quatmann; Enno Ruijters (TACAS (1), 2019)

Probabilistic planning with formal performance guarantees for mobile service robots. - Bruno Lacerda; Fatma Faruq; David Parker 001; Nick Hawes (Int. J. Robotics Res., 2019)

Software Adaptation for an Unmanned Undersea Vehicle. - Avi Pfeffer; Curt Wu; Gerald Fry; Kenny Lu; Steve Marotta; Michael Reposa; Yuan Shi; T. K. Satish Kumar; Craig A. Knoblock; David Parker 001; Irfan Muhammad; Chris Novakovic (IEEE Softw., 2019)

PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (CAV (2), 2020)

Quantitative Verification of Certificate Transparency Gossip Protocols. - Michael Oxford; David Parker 001; Mark Ryan 001 (CNS, 2020)

Probabilistic Guarantees for Safe Deep Reinforcement Learning. - Edoardo Bacci; David Parker 001 (FORMATS, 2020)

On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. - Carlos E. Budde; Arnd Hartmanns; Michaela Klauck; Jan Kretínský; David Parker 001; Tim Quatmann; Andrea Turrini; Zhen Zhang 006 (ISoLA (4), 2020)

Multi-player Equilibria Verification for Concurrent Stochastic Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (QEST, 2020)

ATEN: And/Or tree ensemble for inferring accurate Boolean network topology and dynamics. - Ning Shi; Zexuan Zhu; Ke Tang 001; David Parker 001; Shan He 001 (Bioinform., 2020)

Optimal Online Dispatch for High-Capacity Shared Autonomous Mobility-on-Demand Systems. - Cheng Li; David Parker 001; Qi Hao (ICRA, 2021)

Verifying Reinforcement Learning up to Infinity. - Edoardo Bacci; Mirco Giacobbe; David Parker 001 (IJCAI, 2021)

Vehicle Dispatch in On-Demand Ride-Sharing with Stochastic Travel Times. - Cheng Li; David Parker 001; Qi Hao (IROS, 2021)

Fault diagnosis in labelled Petri nets: A Fourier-Motzkin based approach. - Ahmed Al-Ajeli; David Parker 001 (Autom., 2021)

Quantitative verification of Kalman filters. - Alexandros Evangelidis; David Parker 001 (Formal Aspects Comput., 2021)

Automatic verification of concurrent stochastic systems. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (Formal Methods Syst. Des., 2021)

Introduction to the Special Issue on QEST 2019. - David Parker 001; Verena Wolf (ACM Trans. Model. Comput. Simul., 2021)

Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise. - Thom S. Badings; Alessandro Abate; Nils Jansen 001; David Parker 001; Hasan A. Poonawala; Mariëlle Stoelinga (AAAI, 2022)

Symbolic Verification and Strategy Synthesis for Turn-Based Stochastic Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (Principles of Systems Design, 2022)

Multi-Objective Controller Synthesis with Uncertain Human Preferences. - Shenghui Chen; Kayla Boggess; David Parker 001; Lu Feng 001 (ICCPS, 2022)

A Value-based Dynamic Learning Approach for Vehicle Dispatch in Ride-Sharing. - Cheng Li; David Parker 001; Qi Hao (IROS, 2022)

Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk). - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos; Rui Yan 002 (MFCS, 2022)

Verified Probabilistic Policies for Deep Reinforcement Learning. - Edoardo Bacci; David Parker 001 (NFM, 2022)

Robust Anytime Learning of Markov Decision Processes. - Marnix Suilen; Thiago D. Simão; David Parker 001; Nils Jansen 001 (NeurIPS, 2022)

Correlated Equilibria and Fairness in Concurrent Stochastic Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (TACAS (2), 2022)

Finite-horizon equilibria for neuro-symbolic concurrent stochastic games. - Rui Yan 002; Gabriel Santos; Xiaoming Duan; David Parker 001; Marta Kwiatkowska (UAI, 2022)

Probabilistic Model Checking and Autonomy. - Marta Kwiatkowska; Gethin Norman; David Parker 001 (Annu. Rev. Control. Robotics Auton. Syst., 2022)

Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos; Rui Yan 002 (CoRR, 2022)

Partially-Observable Security Games for Automating Attack-Defense Analysis. - Narges Khakpour; David Parker 001 (CoRR, 2022)

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020. - Armin Biere; David Parker 001 (Int. J. Softw. Tools Technol. Transf., 2022)

Planning for Automated Vehicles with Human Trust. - Shili Sheng; Erfan Pakdamanian; Kyungtae Han; Ziran Wang; John Lenneman; David Parker 001; Lu Feng 001 (ACM Trans. Cyber Phys. Syst., 2022)

Using Reed-Muller Codes for Classification with Rejection and Recovery. - Daniel Fentham; David Parker 001; Mark Ryan 001 (FPS (1), 2023)

Multi-agent Verification and Control with Probabilistic Model Checking. - David Parker 001 (QEST, 2023)

Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (TOOLympics@ETAPS, 2023)

Point-based Value Iteration for Neuro-Symbolic POMDPs. - Rui Yan 002; Gabriel Santos; Gethin Norman; David Parker 001; Marta Kwiatkowska (CoRR, 2023)

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions. - Thom S. Badings; Licio Romao; Alessandro Abate; David Parker 001; Hasan A. Poonawala; Mariëlle Stoelinga; Nils Jansen 001 (J. Artif. Intell. Res., 2023)

Artifact for: Distributional Probabilistic Model Checking. - Ingy Elsayed-Aly; David Parker 001; Lu Feng 001 (Zenodo, 2023)

Artifact for: Distributional Probabilistic Model Checking. - Ingy Elsayed-Aly; David Parker 001; Lu Feng 001 (Zenodo, 2023)

The Hamiltonian Cycle and Travelling Salesperson problems with traversal-dependent edge deletion. - Sarah Carmesin; David Woller; David Parker 001; Miroslav Kulich; Masoumeh Mansouri (J. Comput. Sci., 2023)

Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe. - Hubert Garavel; Holger Hermanns; David Parker 001 (Principles of Verification (2), 2024)

Expectation vs. Reality: Towards Verification of Psychological Games. - Marta Kwiatkowska; Gethin Norman; David Parker 001; Gabriel Santos (Principles of Verification (2), 2024)

Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet. - Marnix Suilen; Thom S. Badings; Eline M. Bovy; David Parker 001; Nils Jansen 001 (Principles of Verification (3), 2024)

Partially Observable Stochastic Games with Neural Perception Mechanisms. - Rui Yan 002; Gabriel Santos; Gethin Norman; David Parker 001; Marta Kwiatkowska (FM (1), 2024)

Safe POMDP Online Planning via Shielding. - Shili Sheng; David Parker 001; Lu Feng 001 (ICRA, 2024)

HSVI-based online minimax strategies for partially observable stochastic games with neural perception mechanisms. - Rui Yan 002; Gabriel Santos; Gethin Norman; David Parker 001; Marta Kwiatkowska (L4DC, 2024)

Distributional Probabilistic Model Checking. - Ingy Elsayed-Aly; David Parker 001; Lu Feng 001 (NFM, 2024)

Partially-Observable Security Games for Attack-Defence Analysis in Software Systems. - Narges Khakpour; David Parker 001 (SEFM, 2024)

Tools at the Frontiers of Quantitative Verification. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (CoRR, 2024)

Learning Provably Robust Policies in Uncertain Parametric Environments. - Yannik Schnitzer; Alessandro Abate; David Parker 001 (CoRR, 2024)

Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games. - Rui Yan 002; Gabriel Santos; Gethin Norman; David Parker 001; Marta Kwiatkowska (Inf. Comput., 2024)

Safe POMDP Online Planning Among Dynamic Agents via Adaptive Conformal Prediction. - Shili Sheng; Pian Yu; David Parker 001; Marta Kwiatkowska; Lu Feng 001 (IEEE Robotics Autom. Lett., 2024)

A Framework for Simultaneous Task Allocation and Planning under Uncertainty. - Fatma Faruq; Bruno Lacerda; Nick Hawes; David Parker 001 (ACM Trans. Auton. Adapt. Syst., 2024)

Robust Probabilistic Bisimilarity for Labelled Markov Chains. - Syyeda Zainab Fatmi; Stefan Kiefer; David Parker 001; Franck van Breugel (CAV (2), 2025)

Certifiably Robust Policies for Uncertain Parametric Environments. - Yannik Schnitzer; Alessandro Abate; David Parker 001 (TACAS (3), 2025)

Learning Algorithms for Verification of Markov Decision Processes. - Tomás Brázdil; Krishnendu Chatterjee; Martin Chmelik; Vojtech Forejt; Jan Kretínský; Marta Kwiatkowska; Tobias Meggendorfer; David Parker 001; Mateusz Ujma (TheoretiCS, 2025)

Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty. - Pian Yu; Yong Li 031; David Parker 001; Marta Kwiatkowska (CoRR, 2025)

Learning Probabilistic Temporal Logic Specifications for Stochastic Systems. - Rajarshi Roy 002; Yash Pote; David Parker 001; Marta Kwiatkowska (CoRR, 2025)

Efficient Solution and Learning of Robust Factored MDPs. - Yannik Schnitzer; Alessandro Abate; David Parker 001 (CoRR, 2025)