Dave Parker's Publications

• [KP12] M. Kwiatkowska and D. Parker. Advances in Probabilistic Model Checking. In Proc. 2011 Marktoberdorf Summer School: Tools for Analysis and Verification of Software Safety and Security, IOS Press. To appear. 2012. [pdf] [bib]
• [LPC+12] M. Lakin, D. Parker, L. Cardelli, M. Kwiatkowska and A. Phillips. Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking. Journal of the Royal Society Interface. To appear. 2012. [pdf] [bib]
• [JKNP12] J. Júlvez, M. Kwiatkowska, G. Norman and D. Parker. Evaluation of Sustained Stochastic Oscillations by Means of a System of Differential Equations. International Journal of Computers and Applications (IJCA). To appear. 2012. [pdf] [bib]
• [CFK+12] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker and A. 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]

• [FHKP11] L. Feng, T. Han, M. Kwiatkowska and D. 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]
• [HNP+11] E. M. Hahn, G. Norman, D. Parker, B. Wachter and L. 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] T. Chen, M. Kwiatkowska, D. Parker and A. 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]
• [KNP11] M. Kwiatkowska, G. Norman and D. 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]
• [KPQ11] M. Kwiatkowska, D. Parker and H. 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]
• [FKNP11] V. Forejt, M. Kwiatkowska, G. Norman and D. 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]
• [FKN+11] V. Forejt, M. Kwiatkowska, G. Norman, D. Parker and H. 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]
• [FKP11] L. Feng, M. Kwiatkowska and D. 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]
• [JKNP11] J. Júlvez, M. Kwiatkowska, G. Norman and D. 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]

• [KNP10c] M. Kwiatkowska, G. Norman and D. 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]
• [KNP10b] M. Kwiatkowska, G. Norman and D. 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]
• [KKNP10] M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker. A Game-based Abstraction-Refinement Framework for Markov Decision Processes. Formal Methods in System Design, 36(3), pages 246-280, Springer. September 2010. [pdf] [bib]
• [FKP10] L. Feng, M. Kwiatkowska and D. 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]
• [KNP10a] M. Kwiatkowska, G. Norman and D. 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]
• [KNPQ10] M. Kwiatkowska, G. Norman, D. Parker and H. 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]
• [DKN+10] M. Duflot, M. Kwiatkowska, G. Norman, D. Parker, S. Peyronnet, C. Picaronny and J. 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, IEEE Computer Society Press. To appear. 2010. [pdf] [bib]

• [KNP09c] M. Kwiatkowska, G. Norman and D. 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]
• [DMP09] A. Donaldson, A. Miller and D. 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]
• [KNP09b] M. Kwiatkowska, G. Norman and D. 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]
• [NPPW09] G. Norman, C. Palamidessi, D. Parker and P. Wu. Model Checking Probabilistic and Stochastic Extensions of the Pi-Calculus. IEEE Transactions on Software Engineering, 35(2), pages 209-223, IEEE Computer Society. March 2009. [pdf] [bib]
• [KNPV09] M. Kwiatkowska, G. Norman, D. Parker and M.G. Vigliotti. Probabilistic Mobile Ambients. Theoretical Computer Science, 410(12-13), pages 1272-1303, Elsevier. March 2009. [ps.gz] [pdf] [bib]
• [CNP09] K. Chatzikokolakis, G. Norman and D. 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]
• [KNP09a] M. Kwiatkowska, G. Norman and D. Parker. PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4), pages 40-45, ACM. March 2009. [pdf] [bib]
• [KKNP09] M. Kattenbelt, M. Kwiatkowska, G. Norman and D. 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]

• [KNP08d] M. Kwiatkowska, G. Norman and D. Parker. Analysis of a Gossip Protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36(3), pages 17-22. December 2008. [pdf] [bib]
• [RPNdA08] P. Roy, D. Parker, G. Norman and L. 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]
• [CBGP08] F. Ciesinski, C. Baier, M. Groesser and D. 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]
• [KKNP08a] M. Kattenbelt, M. Kwiatkowska, G. Norman and D. 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]
• [KNP08a] M. Kwiatkowska, G. Norman and D. Parker. Using Probabilistic Model Checking in Systems Biology. ACM SIGMETRICS Performance Evaluation Review, 35(4), pages 14-21, Association for Computing Machinery. March 2008. [ps.gz] [pdf] [bib]
• [HKN+08] J. Heath, M. Kwiatkowska, G. Norman, D. Parker and O. Tymchyshyn. Probabilistic Model Checking of Complex Biological Pathways. Theoretical Computer Science (Special Issue on Converging Sciences: Informatics and Biology), 391(3), pages 239-257, Elsevier. February 2008. [ps.gz] [pdf] [bib]
• [KNPS08] M. Kwiatkowska, G. Norman, D. Parker and J. 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]

• [KNP07b] M. Kwiatkowska, G. Norman and D. Parker. Controller Dependability Analysis By Probabilistic Model Checking. Control Engineering Practice, 15(11), pages 1427-1434, Elsevier. November 2007. [ps.gz] [pdf] [bib]
• [DMP07] A. Donaldson, A. Miller and D. 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]
• [NPPW07] G. Norman, C. Palamidessi, D. Parker and P. 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]
• [KNP07a] M. Kwiatkowska, G. Norman and D. 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]

• [GNB+06] M. Groesser, G. Norman, C. Baier, F. Ciesinski, M. Kwiatkowska, D. 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] M. Kwiatkowska, G. Norman, D. Parker, O. Tymchyshyn, J. Heath and E. 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]
• [DKNP06] M. Duflot, M. Kwiatkowska, G. Norman and D. Parker. A Formal Analysis of Bluetooth Device Discovery. International Journal on Software Tools for Technology Transfer (STTT), 8(6), pages 621 - 632, Springer-Verlag. November 2006. [ps.gz] [pdf] [bib]
• [HKN+06] J. Heath, M. Kwiatkowska, G. Norman, D. Parker and O. 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]
• [KNP06b] M. Kwiatkowska, G. Norman and D. 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] M. Kwiatkowska, G. Norman and D. 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]
• [KNPS06] M. Kwiatkowska, G. Norman, D. Parker and J. Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. Formal Methods in System Design, 29, pages 33-78, Springer. August 2006. [ps.gz] [pdf] [bib]
• [YKNP06] H. Younes, M. Kwiatkowska, G. Norman and D. Parker. Numerical vs. Statistical Probabilistic Model Checking. International Journal on Software Tools for Technology Transfer (STTT), 8(3), pages 216-228, Springer. June 2006. [ps.gz] [pdf] [bib]
• [HKNP06] A. Hinton, M. Kwiatkowska, G. Norman and D. 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]

• [NPKS05] G. Norman, D. Parker, M. Kwiatkowska and S. Shukla. Evaluating the Reliability of NAND Multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), pages 1629-1637. October 2005. [ps.gz] [pdf] [bib]
• [KNP05c] M. Kwiatkowska, G. Norman and D. 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]
• [ZPK05b] Y. Zhang, D. Parker and M. Kwiatkowska. Grid-enabled Probabilistic Model Checking with PRISM. In Proc. 4th All Hands Meeting Workshop (AHM'05). September 2005. [ps.gz] [pdf] [bib]
• [NPK+05] G. Norman, D. Parker, M. Kwiatkowska, S. Shukla and R. Gupta. Using Probabilistic Model Checking for Dynamic Power Management. Formal Aspects of Computing, 17(2), pages 160-176, Springer-Verlag. August 2005. [ps.gz] [pdf] [bib]
• [ZPK05a] Y. Zhang, D. Parker and M. 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]
• [KNP05d] M. Kwiatkowska, G. Norman and D. Parker. Quantitative Analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science, 153(2), pages 5-31, Elsevier. May 2005. [ps.gz] [pdf] [bib]
• [KNP05b] M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking in Practice: Case Studies with PRISM. ACM SIGMETRICS Performance Evaluation Review, 32(4), pages 16-21. March 2005. [ps.gz] [pdf] [bib]

• [DKNP04] M. Duflot, M. Kwiatkowska, G. Norman and D. 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]
• [KPZM04] M. Kwiatkowska, D. Parker, Y. Zhang and R. 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] M. Kwiatkowska, G. Norman and D. 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]
• [KNP04b] M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2), pages 128-142. September 2004. [ps.gz] [pdf] [bib]
• [MP04] A. Miner and D. 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]
• [KNP04c] M. Kwiatkowska, G. Norman and D. 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]
• [KNP04a] J. Rutten, M. Kwiatkowska, G. Norman and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. Volume 23 of CRM Monograph Series. American Mathematical Society. P. Panangaden and F. van Breugel (eds.). March 2004. [bib]
• [YKNP04] H. Younes, M. Kwiatkowska, G. Norman and D. 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] G. Norman, D. Parker, M. Kwiatkowska and S. 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]

• [MPK03b] R. Mehmood, D. Parker and M. Kwiatkowska. An Efficient BDD-Based Implementation of Gauss-Seidel for CTMC Analysis. Technical report CSR-03-13, School of Computer Science, University of Birmingham. December 2003. [ps.gz] [pdf] [bib]
• [KNPS03] M. Kwiatkowska, G. Norman, D. Parker and J. 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]
• [MPK03a] R. Mehmood, D. Parker and M. Kwiatkowska. An Efficient Symbolic Out-of-Core Solution Method for Markov Models. Technical report CSR-03-08, School of Computer Science, University of Birmingham. August 2003. [ps.gz] [pdf] [bib]
• [HKN+03] H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker and M. Siegle. On the use of MTBDDs for Performability Analysis and Verification of Stochastic Systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56, pages 23-67, Elsevier. June 2003. [ps.gz] [pdf] [bib]
• [NPK+03] G. Norman, D. Parker, M. Kwiatkowska, S. Shukla and R. 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]

• [NPK+02] G. Norman, M. Kwiatkowska, D. Parker, S. Shukla and R. 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]
• [Par02] D. Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham. August 2002. [ps.gz] [pdf] [bib]
• [KMNP02] M. Kwiatkowska, R. Mehmood, G. Norman and D. 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] M. Kwiatkowska, G. Norman and D. 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] M. Kwiatkowska, G. Norman and D. 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]

• [KKNP01] J.-P. Katoen, M. Kwiatkowska, G. Norman and D. 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] M. Kwiatkowska, G. Norman and D. 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]

• [KNP00] M. Kwiatkowska, G. Norman and D. Parker. Verifying Randomized Distributed Algorithms with PRISM. In Proc. Workshop on Advances in Verification (Wave'2000). July 2000. [ps.gz] [pdf] [bib]
• [dAKN+00] L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker and R. 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]