David Parker
Reader, Computer Science, University of Birmingham

Publications

Here is a full list of my publications. In the majority of cases, author ordering is alphabetical.

See also my pages on DBLP, Google Scholar, Scopus or ORCID.

122 publications:

Books and edited volumes

Book chapters

  • [KNP17] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking: Advances and Applications. In R. Drechsler (editor), Formal System Verification, pages 73-121, Springer. June 2017. [pdf] [bib] [Provides an introduction to probabilistic model checking, including coverage of some recent advances in the field and a wide variety of examples and applications.]
  • [DKN+13] Marie Duflot, Marta Kwiatkowska, Gethin Norman, David Parker, Sylvain Peyronnet, Claudine Picaronny and Jeremy Sproston. Practical Applications of Probabilistic Model Checking to Communication Protocols. In S. Gnesi and T. Margaria (editors), Formal Methods for Industrial Critical Systems: A Survey of Applications, pages 133-150, IEEE Computer Society Press. March 2013. [pdf] [bib] [Applies PRISM and APMC to analyse the IEEE 802.3 (CSMA/CD) protocol.]
  • [KP12] Marta Kwiatkowska and David Parker. Advances in Probabilistic Model Checking. In Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 126-151, IOS Press. June 2012. [pdf] [bib] [Tutorial paper on probabilistic model checking, covering DTMCs, MDPs, quantitative abstraction refinement, PTAs and PRISM.]
  • [FKNP11] Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman and David Parker. Automated Verification Techniques for Probabilistic Systems. In M. Bernardo and V. Issarny (editors), Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of LNCS, pages 53-113, Springer. June 2011. [pdf] [bib] [Tutorial paper on probabilistic model checking, focusing on verification techniques for MDPs, accompanied by case studies and examples for PRISM.]
  • [KNP10a] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking for Systems Biology. In M. Sriram Iyengar (editor), Symbolic Systems Biology, pages 31-59, Jones and Bartlett. May 2010. [pdf] [bib] [Tutorial on the application of probabilistic model checking and PRISM to systems biology, including an illustrative case study (FGF) and reader exercises.]
  • [KNP09b] Marta Kwiatkowska, Gethin Norman and David Parker. Quantitative Verification Techniques for Biological Processes. In A. Condon, D. Harel, J. Kok, A. Salomaa and E. Winfree (editors), Algorithmic Bioprocesses, pages 391-409, Springer. August 2009. [pdf] [bib] [Tutorial paper on the application of probabilistic model checking and PRISM to biological systems, including an illustrative case study (MAPK cascade).]
  • [KNPS08] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Verification of Real-Time Probabilistic Systems. In S. Merz and N. Navet (editors), Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 249-288, John Wiley & Sons. January 2008. [pdf] [bib] http://www.iste.co.uk/index.php?p=a&ACTION=View&id=195 [Tutorial on probabilistic timed automata (PTAs) and the methods used by PRISM to analyse them.]
  • [KNP07a] Marta Kwiatkowska, Gethin Norman and David Parker. Stochastic Model Checking. In M. Bernardo and J. Hillston (editors), Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer. June 2007. [pdf] [bib] [Tutorial paper covering probabilistic model checking of DTMCs/CTMCs and PRISM.]
  • [MP04] Andrew Miner and David Parker. Symbolic Representations and Analysis of Large Probabilistic Systems. In C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen, M. Siegle and F. Vaandrager (editors), Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 296-338. August 2004. [ps.gz] [pdf] [bib] [Tutorial/survey paper on symbolic methods for probabilistic verification, including the (MD)BDD-based methods in PRISM.]

Journal papers

Conference papers

  • [FLHP18] Fatma Faruq, Bruno Lacerda, Nick Hawes and David Parker. Simultaneous Task Allocation and Planning Under Uncertainty. In Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'18), IEEE. To appear. October 2018. [pdf] [bib] [Proposes techniques for verified multi-robot task allocation and planning, implemented as an extension of PRISM.]
  • [KNPS18] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Automated Verification of Concurrent Stochastic Games. In Proc. 15th International Conference on Quantitative Evaluation of SysTems (QEST'18). To appear. September 2018. [pdf] [bib] [Proposes verification techniques for concurrent stochastic games, and implements and evaluates them in an extension of PRISM-games.]
  • [AP18] Ahmed Al-Ajeli and David Parker. Online fault diagnosis in Petri net models of discrete-event systems using Fourier-Motzkin. In Proc. 12th UKACC International Conference on Control, IEEE. To appear. September 2018. [pdf] [bib]
  • [KNP17b] Marta Kwiatkowska, Gethin Norman and David Parker. Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In Models, Algorithms, Logics and Tools, volume 10460 of LNCS, pages 289-309, Springer. August 2017. [pdf] [bib] [Proposes novel symbolic techniques for verifi cation and optimal strategy synthesis for priced probabilistic timed automata ]
  • [BKLPW17] Christel Baier, Joachim Klein, Linda Leuschner, David Parker and Sascha Wunderlich. Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In Proc. 28th International Conference on Computer Aided Verification (CAV'17), volume 10426 of LNCS, pages 160-180, Springer. July 2017. [pdf] [bib] [Proposes "interval iteration" techniques for deriving more accurate bounds on the results of probabilistic model checking, and implements them in PRISM.]
  • [LPH17] Bruno Lacerda, David Parker and Nick Hawes. Multi-objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees. In Proc. 27th International Conference on Automated Planning and Scheduling (ICAPS'17), pages 504-512, AAAI Press. June 2017. [pdf] [bib] [Proposes techniques for generating mobile robot controllers with probabilistic time-bounded guarantees using multi-objective probabilistic model checking and an extension of PRISM.]
  • [EPB17] Alexandros Evangelidis, David Parker and Rami Bahsoon. Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. In Proc. IEEE/ACM 17th International Symposium on Cluster, Cloud and Grid Computing (CCGrid'17), pages 355-364, IEEE. May 2017. [pdf] [bib] [Presents an approach for producing formal performance guarantees for cloud-based auto-scaling policies using PRISM.]
  • [MDPR16] Chunyan Mu, Peter Dittrich, David Parker and Jonathan E. Rowe. Formal Quantitative Analysis of Reaction Networks Using Chemical Organisation Theory. In Proc. 14th International Conference on Computational Methods in Systems Biology (CMSB'16), volume 9859 of LNCS, pages 232-251, Springer. September 2016. [pdf] [bib] [Develops techniques for analysing reaction networks using chemical organisation theory, implemented in an extension of PRISM.]
  • [ANP16] Zaruhi Aslanyan, Flemming Nielson and David Parker. Quantitative Verification and Synthesis of Attack-Defence Scenarios. In Proc. 29th IEEE Computer Security Foundations Symposium (CSF'16), pages 105-119, IEEE. June 2016. [pdf] [bib] [Proposes formal verification techniques for attack-defence scenarios based on model checking of stochastic games and building on the PRISM-games tool.]
  • [KPW16] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), volume 9636 of LNCS, pages 560-566, Springer. April 2016. [pdf] [bib] [Introduces version 2.0 of the PRISM-games tool.]
  • [KPR16] Nishanthan Kamaleson, David Parker and Jonathan E. Rowe. Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. In Proc. 2016 International Symposium on Model Checking of Software (SPIN'16), volume 9641 of LNCS, pages 147-164, Springer. April 2016. [pdf] [bib] [Proposes a finite-horizon variant of probabilistic bisimulation and implements various associated minimisation algorithms in an extension of PRISM.]
  • [LPH15b] Bruno Lacerda, David Parker and Nick Hawes. Nested Value Iteration for Partially Satisfiable Co-Safe LTL Specifications (Extended Abstract). In Proc. AAAI Fall Symposium on Sequential Decision Making for Intelligent Agents (SDMIA), pages 54-55. November 2015. [pdf] [bib]
  • [NPZ15] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Real-Time Systems. In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of LNCS, pages 240-255, Springer. September 2015. [pdf] [bib] [Develops techniques for verification and controller synthesis on a partially observable variant of probabilistic timed automata, implemented in an extension of PRISM.]
  • [LPH15] Bruno Lacerda, David Parker and Nick Hawes. Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications. In Proc. 24th International Joint Conference on Artificial Intelligence (IJCAI'15), pages 1587-1593, IJCAI/AAAI. August 2015. [pdf] [bib] [Proposes techniques for synthesising optimal policies in MDPs, building on multi-objective probabilistic model checking and PRISM, and applies them to robot task planning.]
  • [BBDL+15] Tomas Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretinsky, David Muller, David Parker and Jan Strejcek. The Hanoi Omega-Automata Format. In Proc. 27th International Conference on Computer Aided Verification (CAV'15), volume 9206 of LNCS, pages 479-486, Springer. July 2015. [pdf] [bib] [Proposes an exchange format for omega automata, and describes implemented support in a variety of tools, including PRISM.]
  • [BCC+14] Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelík, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, David Parker and Mateusz Ujma. Verification of Markov Decision Processes using Learning Algorithms. In Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA'14), volume 8837 of LNCS, pages 98-114, Springer. November 2014. [pdf] [bib] [Presents MDP verification techniques, implemented in PRISM, based on real-time dynamic programming and delayed Q-learning.]
  • [LPH14b] Bruno Lacerda, David Parker and Nick Hawes. Optimal and Dynamic Planning for Markov Decision Processes with Co-Safe LTL Specifications. In Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'14), pages 1511-1516, IEEE. September 2014. [pdf] [bib] [Proposes a dynamic planning approach for co-safe LTL, implements it in an extension of PRISM and deploys it on a mobile service robot.]
  • [AKNP14] Alessandro Abate, Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations. In F. van Breugel, E. Kashefi, C. Palamidessi and J. Rutten (editors), Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of LNCS, pages 40-58, Springer. May 2014. [pdf] [bib] [Performs probabilistic model checking on continuous-state models using a finite-state abstraction which is then passed to PRISM.]
  • [DFK+14] Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of LNCS, pages 531-546, Springer. April 2014. [pdf] [bib] [Presents permissive controller synthesis techniques for stochastic games, implemented in an extension of PRISM.]
  • [KPQU14] Marta Kwiatkowska, David Parker, Hongyang Qu and Mateusz Ujma. On Incremental Quantitative Verification for Probabilistic Systems. In Andrei Voronkov and Margarita Korovina (editors), HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, pages 245-257, Easychair. February 2014. [pdf] [bib] http://www.easychair.org/publications/?page=195264436 [Describes incremental methods for runtime probabilistic model checking, implemented in an extension of PRISM.]
  • [LPH14a] Bruno Lacerda, David Parker and Nick Hawes. Optimal Motion Planning for Markov Decision Processes with Co-Safe Linear Temporal Logic Specifications. In Proc. 31st Workshop of the UK Planning & Scheduling Special Interest Group (PlanSIG). January 2014. [pdf] [bib]
  • [KP13] Marta Kwiatkowska and David Parker. Automated Verification and Strategy Synthesis for Probabilistic Systems. In Proc. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of LNCS, pages 5-22, Springer. October 2013. [pdf] [bib] [Provides an overview of strategy synthesis techniques for probabilistic models.]
  • [Par13] David Parker. Verification of Probabilistic Real-time Systems. In Proc. 2013 Real-time Systems Summer School (ETR'13). August 2013. [pdf] [A short overview of probabilistic model checking for probabilistic real-time systems.]
  • [CKNP13] Tom Chothia, Yusuke Kawamoto, Chris Novakovic and David Parker. Probabilistic Point-to-Point Information Leakage. In Proc. 26th IEEE Computer Security Foundations Symposium (CSF'13), pages 193-205. June 2013. [pdf] [bib]
  • [CFK+13] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of LNCS, pages 185-191, Springer. March 2013. [pdf] [bib] [Introduces PRISM-games, a model checker for stochastic multi-player games.]
  • [KPS13] Marta Kwiatkowska, David Parker and Aistis Simaitis. Strategic Analysis of Trust Models for User-Centric Networks. In Proc. 1st International Workshop on Strategic Reasoning (SR'13), volume 112 of EPTCS, pages 53-60. March 2013. [pdf] [bib] [Analyses a cooperation model for user-centric networks using PRISM-games.]
  • [DKP13] Christian Dehnert, Joost-Pieter Katoen and David Parker. SMT-Based Bisimulation Minimisation of Markov Models. In Proc. 14th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), volume 7737 of LNCS, pages 28-47, Springer. January 2013. [pdf] [bib] [Presents new SMT-based bisimulation techniques for Markov chains expressed in the PRISM modelling language.]
  • [FKP12] Vojtěch Forejt, Marta Kwiatkowska and David Parker. Pareto Curves for Probabilistic Model Checking. In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 317-332, Springer. October 2012. [pdf] [bib] [Describes new techniques for multi-objective probabilistic model checking using Pareto curves, implemented in PRISM.]
  • [KNP12b] Marta Kwiatkowska, Gethin Norman and David Parker. The PRISM Benchmark Suite. In Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST'12), pages 203-204, IEEE CS Press. September 2012. [pdf] [bib] [Introduces a suite of PRISM models/properties and other resources for benchmarking and testing.]
  • [FKP+12] Vojtěch Forejt, Marta Kwiatkowska, David Parker, Hongyang Qu and Mateusz Ujma. Incremental Runtime Verification of Probabilistic Systems. In Proc. 3rd International Conference on Runtime Verification (RV'12), volume 7686 of LNCS, pages 314-319, Springer. September 2012. [pdf] [bib] [Proposes incremental methods for runtime probabilistic model checking, implemented in an extension of PRISM.]
  • [CFK+12] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 315-330, Springer. March 2012. [pdf] [bib] [Introduces model checking techniques for stochastic multi-player games, implemented in the PRISM-games tool.]
  • [FHKP11] Lu Feng, Tingting Han, Marta Kwiatkowska and David Parker. Learning-based Compositional Verification for Synchronous Probabilistic Systems. In Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), volume 6996 of LNCS, pages 511-521, Springer. October 2011. [pdf] [bib] [Presents a learning-based compositional verification framework which uses PRISM for executing individual queries.]
  • [HNP+11] Ernst Moritz Hahn, Gethin Norman, David Parker, Bjorn Wachter and Lijun Zhang. Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST'11), pages 69-78, IEEE CS Press. September 2011. [pdf] [bib]
  • [CKPS11] Taolue Chen, Marta Kwiatkowska, David Parker and Aistis Simaitis. Verifying Team Formation Protocols with Probabilistic Model Checking. In Proc. 12th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XII 2011), volume 6814 of LNCS, pages 190-297, Springer. July 2011. [pdf] [bib] [Analyses a team formation protocol using PRISM and a prototype extension for stochastic games.]
  • [KNP11] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of LNCS, pages 585-591, Springer. July 2011. [pdf] [bib] [Tool paper describing PRISM 4.0.]
  • [KPQ11] Marta Kwiatkowska, David Parker and Hongyang Qu. Incremental Quantitative Verification for Markov Decision Processes. In Proc. IEEE/IFIP International Conference on Dependable Systems and Networks (DSN-PDS'11), pages 359-370, IEEE CS Press. June 2011. [pdf] [bib] [Presents incremental verification techniques for MDPs, implemented as an extension of PRISM.]
  • [JKNP11] Jorge Júlvez, Marta Kwiatkowska, Gethin Norman and David Parker. A Systematic Approach to Evaluate Sustained Stochastic Oscillations. In H. Al-Mubaid (editor), Proc. ISCA 3rd International Conference on Bioinformatics and Computational Biology (BICoB'11), pages 134-139, ISCA. March 2011. [pdf] [bib]
  • [FKP11] Lu Feng, Marta Kwiatkowska and David Parker. Automated Learning of Probabilistic Assumptions for Compositional Reasoning. In Proc. 14th International Conference on Fundamental Approaches to Software Engineering (FASE'11), volume 6603 of LNCS, pages 2-17, Springer. Invited paper. March 2011. [pdf] [bib] [Presents a learning-based compositional verification framework, based on an extension of PRISM.]
  • [FKN+11] Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu. Quantitative Multi-Objective Verification for Probabilistic Systems. In Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 of LNCS, pages 112-127, Springer. March 2011. [pdf] [bib] [Presents multi-objective and assume-guarantee verification techniques for probabilistic automata, implemented as an extension of PRISM.]
  • [KNP10c] Marta Kwiatkowska, Gethin Norman and David Parker. Advances and Challenges of Probabilistic Model Checking. In Proc. 48th Annual Allerton Conference on Communication, Control and Computing, pages 1691-1698, IEEE Press. Invited paper. October 2010. [pdf] [bib] [Gives a high-level overview of probabilistic model checking and PRISM; and surveys some current recent directions.]
  • [FKP10] Lu Feng, Marta Kwiatkowska and David Parker. Compositional Verification of Probabilistic Systems using Learning. In Proc. 7th International Conference on Quantitative Evaluation of Systems (QEST'10), pages 133-142, IEEE CS Press. September 2010. [pdf] [bib] [Presents a learning-based compositional verification framework, based on an extension of PRISM.]
  • [KNP10b] Marta Kwiatkowska, Gethin Norman and David Parker. A Framework for Verification of Software with Time and Probabilities. In Proc. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of LNCS, pages 25-45, Springer. September 2010. [pdf] [bib] [Extends PRISM's game-based abstraction-refinement methods for PTAs, to real-time probabilistic programs with data.]
  • [KNPQ10] Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu. Assume-Guarantee Verification for Probabilistic Systems. In Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), volume 6015 of LNCS, pages 23-37, Springer. March 2010. [pdf] [bib] [Presents assume-guarantee verification techniques for probabilistic automata, implemented as an extension of PRISM.]
  • [KNP09c] Marta Kwiatkowska, Gethin Norman and David Parker. Stochastic Games for Verification of Probabilistic Timed Automata. In Proc. 7th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'09), volume 5813 of LNCS, pages 212-227, Springer. September 2009. [pdf] [bib] [Presents game-based abstraction-refinement techniques for verifying PTAs, implemented in PRISM.]
  • [DMP09] Alastair Donaldson, Alice Miller and David Parker. Language-level Symmetry Reduction for Probabilistic Model Checking. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), pages 289-298, IEEE Computer Society. September 2009. [pdf] [bib] [Presents symmetry reduction techniques based on translation of PRISM models.]
  • [CNP09] Kostas Chatzikokolakis, Gethin Norman and David Parker. Bisimulation for Demonic Schedulers. In Proc. 12th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'09), volume 5504 of LNCS, pages 318-332, Springer. March 2009. [ps.gz] [pdf] [bib]
  • [KKNP09] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. Abstraction Refinement for Probabilistic Software. In Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), volume 5403 of Lecture Notes in Computer Science, pages 182-197, Springer. January 2009. [ps.gz] [pdf] [bib] [Develops verification techniques for probabilistic C programs, using components from GOTO-CC, SATABS and PRISM.]
  • [RPNdA08] Pritam Roy, David Parker, Gethin Norman and Luca de Alfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST'08), pages 103-112, IEEE CS Press. September 2008. [pdf] [bib] [Presents a symbolic version of magnifying lens abstraction, implemented as an extension of PRISM.]
  • [CBGP08] Frank Ciesinski, Christel Baier, Marcus Groesser and David Parker. Generating Compact MTBDD-Representations from Probmela Specifications. In Proc. 15th International SPIN Workshop on Model Checking of Software (SPIN'08), volume 5156 of Lecture Notes in Computer Science, pages 60-76, Springer. August 2008. [pdf] [bib] [Presents techniques for efficient translation of Probmela models into the PRISM modelling language.]
  • [KKNP08a] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. Game-Based Probabilistic Predicate Abstraction in PRISM. In Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08), volume 220 (3) of Electronic Notes in Theoretical Computer Science , pages 5-21 , Elsevier. March 2008. [ps.gz] [pdf] [bib] [Develops predicate abstraction techniques for PRISM, using SMT and game-based abstraction.]
  • [NPPW07] Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking the Probabilistic Pi-calculus. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 169-178, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents model checking techniques for the probabilistic pi-calculus based on a translation to PRISM.]
  • [DMP07] Alastair Donaldson, Alice Miller and David Parker. GRIP: Generic Representatives in PRISM. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 115-116, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents GRIP, a symmetry reduction tool for PRISM models.]
  • [GNB+06] Marcus Groesser, Gethin Norman, Christel Baier, Frank Ciesinski, Marta Kwiatkowska, David Parker. On reduction criteria for probabilistic reward models. In S. Arun-Kumar and N. Garg (editors), Proc. 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), volume 4337 of Lecture Notes in Computer Science, pages 309-320, Springer Verlag. December 2006. [ps.gz] [pdf] [bib]
  • [KNP+06] Marta Kwiatkowska, Gethin Norman, David Parker, Oksana Tymchyshyn, John Heath and Eamonn Gaffney. Simulation and Verification for Computational Modelling of Signalling Pathways. In Proc. 2006 Winter Simulation Conference, pages 1666-1674. December 2006. [ps.gz] [pdf] [bib]
  • [HKN+06] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. In C. Priami (editor), Proc. Computational Methods in Systems Biology (CMSB'06), volume 4210 of Lecture Notes in Bioinformatics, pages 32-47, Springer Verlag. October 2006. [ps.gz] [pdf] [bib] [Analyses the FGF (Fibroblast Growth Factor) signalling pathway using PRISM.]
  • [KNP06b] Marta Kwiatkowska, Gethin Norman and David Parker. Game-based Abstraction for Markov Decision Processes. In Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pages 157-166, IEEE CS Press. Winner of the QEST'06 Best Paper Award. September 2006. [ps.gz] [pdf] [bib]
  • [KNP06a] Marta Kwiatkowska, Gethin Norman and David Parker. Symmetry Reduction for Probabilistic Model Checking. In T. Ball and R. Jones (editors), Proc. 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 234-248, Springer-Verlag. August 2006. [ps.gz] [pdf] [bib]
  • [HKNP06] Andrew Hinton, Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In H. Hermanns and J. Palsberg (editors), Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), volume 3920 of Lecture Notes in Computer Science, pages 441-444, Springer. March 2006. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]
  • [KNP05c] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking and Power-Aware Computing. In In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), pages 6-9. September 2005. [ps.gz] [pdf] [bib] [Applies PRISM to the analysis of power-aware systems: dynamic power management and dynamic voltage scaling.]
  • [ZPK05b] Yi Zhang, David Parker and Marta Kwiatkowska. Grid-enabled Probabilistic Model Checking with PRISM. In Proc. 4th All Hands Meeting Workshop (AHM'05). September 2005. [ps.gz] [pdf] [bib]
  • [ZPK05a] Yi Zhang, David Parker and Marta Kwiatkowska. A Wavefront Parallelisation of CTMC Solution using MTBDDs. In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 732-742, IEEE CS Press. June 2005. [ps.gz] [pdf] [bib]
  • [DKNP04] Marie Duflot, Marta Kwiatkowska, Gethin Norman and David Parker. A Formal Analysis of Bluetooth Device Discovery. In T. Margaria and B. Steffen, A. Philippou and M. Reitenspiess (editors), Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), volume TR-2004-6 of Technical Report, pages 268-275, Department of Computer Science, University of Cyprus. November 2004. [ps.gz] [pdf] [bib] [Analyses device discovery in Bluetooth using PRISM.]
  • [KPZM04] Marta Kwiatkowska, David Parker, Yi Zhang and Rashid Mehmood. Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking. In Proc. 12th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 123-130, IEEE CS Press. October 2004. [ps.gz] [pdf] [bib]
  • [KNP04d] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM 2.0: A Tool for Probabilistic Model Checking. In Proc. 1st International Conference on Quantitative Evaluation of Systems (QEST'04), pages 322-323, IEEE CS Press. September 2004. [ps.gz] [pdf] [bib] [Tool paper describing PRISM 2.0.]
  • [KNP04c] Marta Kwiatkowska, Gethin Norman and David Parker. Controller Dependability Analysis By Probabilistic Model Checking. In Proc. 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'04), pages 177-182, Elsevier. April 2004. [ps.gz] [pdf] [bib] [Illustrates the applicability of probabilistic model checking and PRISM to analysing dependability properties for a simple model of a software-based control systems.]
  • [YKNP04] Håkan Younes, Marta Kwiatkowska, Gethin Norman and David Parker. Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. In K. Jensen and A. Podelski (editors), Proc. TACAS'04, volume 2988 of Lecture Notes in Computer Science, pages 46-60, Springer. March 2004. [ps.gz] [pdf] [bib]
  • [NPKS04] Gethin Norman, David Parker, Marta Kwiatkowska and Sandeep Shukla. Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking. In Proc. International Conference on VLSI Design, pages 907-914, IEEE CS Press. January 2004. [ps.gz] [pdf] [bib] [Analyses the reliability of defect-tolerant design, NAND multiplexing, using PRISM.]
  • [KNPS03] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. In Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 105-120, Springer. September 2003. [ps.gz] [pdf] [bib]
  • [NPK+03] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Using Probabilistic Model Checking for Dynamic Power Management. In Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03). Technical Report DSSE-TR-2003-2, University of Southampton. April 2003. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using PRISM.]
  • [NPK+02] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Formal Analysis and Validation of Continuous Time Markov Chain Based System Level Power Management Strategies. In Proc. 7th Annual IEEE International Workshop on High Level Design Validation and Test (HLDVT'02), pages 45-50, OmniPress. October 2002. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using CTMC models built with PRISM.]
  • [KMNP02] Marta Kwiatkowska, Rashid Mehmood, Gethin Norman and David Parker. A Symbolic Out-of-Core Solution Method for Markov Models. In Proc. Workshop on Parallel and Distributed Model Checking (PDMC'02), volume 68.4 of ENTCS. August 2002. [ps.gz] [pdf] [bib]
  • [KNP02b] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In J-P. Katoen and P. Stevens (editors), Proc. TACAS'02, volume 2280 of Lecture Notes in Computer Science, pages 52-66, Springer. April 2002. [ps.gz] [pdf] [bib]
  • [KNP02a] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: Probabilistic Symbolic Model Checker. In T. Field, P. Harrison, J. Bradley and U. Harder (editors), Proc. TOOLS 2002, volume 2324 of Lecture Notes in Computer Science, pages 200-204, Springer. April 2002. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]
  • [KKNP01] Joost-Pieter Katoen, Marta Kwiatkowska, Gethin Norman and David Parker. Faster and Symbolic CTMC Model Checking. In L. de Alfaro and S. Gilmore (editors), Proc. PAPM/PROBMIV'01, volume 2165 of Lecture Notes in Computer Science, pages 23-38, Springer. September 2001. [ps.gz] [pdf] [bib]
  • [KNP01] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: Probabilistic Symbolic Model Checker. In Proc. PAPM/PROBMIV'01 Tools Session, pages 7-12. Available as Technical Report 760/2001, University of Dortmund. September 2001. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]
  • [KNP00] Marta Kwiatkowska, Gethin Norman and David Parker. Verifying Randomized Distributed Algorithms with PRISM. In Proc. Workshop on Advances in Verification (Wave'2000). July 2000. [ps.gz] [pdf] [bib]
  • [dAKN+00] Luca de Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker and Roberto Segala. Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation. In S. Graf and M. Schwartzbach (editors), Proc. TACAS'00, volume 1785 of Lecture Notes in Computer Science, pages 395-410, Springer. March 2000. [ps.gz] [pdf] [bib]

Theses

Technical reports

Other