PRISM Bibliography

The following is a bibliography of PRISM-related papers. This includes both papers from the PRISM team and from elsewhere. We also have a list of just the external PRISM-related papers. If there is something we have omitted, please contact us.

Sort by: date, type, title

231 publications:

2010

[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), Springer. To appear. March 2010. [pdf] [bib]
[KNP10a] M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking for Systems Biology. In Symbolic Systems Biology, Jones and Bartlett. To appear. 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) FMICS Handbook on Industrial Critical Systems, IEEE Computer Society Press. To appear. 2010. [pdf] [bib]

2009

[BMM09] P. Ballarini, R. Mardare and I. Mura. Analysing Biochemical Oscillation through Probabilistic Model Checking. In Proc. 2nd Workshop From Biology to Concurrency and Back (FBTC'08), volume 229 (issue 1) of Electronic Notes in Theoretical Computer Science, pages 3-19, Elsevier. 2009. [bib]
[CGHV09] M. Calder, S. Gilmore, J. Hillston and V. Vyshemirsky. Formal methods for biochemical signalling pathways. In Formal Methods: State of the Art and New Directions, Springer. To appear. 2009. [bib]
[BM09] C. Berttolini and A. Mota. Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. In Proc. 7th IEEE International Conference on Software Engineering and Formal Methods. 2009. [bib]
[JCL+09] S. Jha, E. Clarke, C. Langmead, A. Legay, A. Platzer and P. Zuliani. A Bayesian approach to model checking biological systems. In Proc. 7th International Conference on Computational Methods in Systems Biology (CMSB'09), Springer. 2009. [bib]
[MS09] J. Misra and I. Saha. A Reinforcement Model for Collaborative Security and Its Formal Analysis. In Proc. New Security Paradigms Workshop (NSPW'09). 2009. [bib]
[BF09] R. Bakhshi and A. Fehnker. On the impact of modelling choices for distributed information spread. A comparative study. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). 2009. [bib]
[AFG+09] H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner and S. Leue. Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). 2009. [bib]
[BGK+09] T. Berczes, G. Guta, G. Kusper, W. Schreiner and J. Sztrik. Analyzing a Proxy Cache Server Performance Model with the Probabilistic Model Checker PRISM. In Proc. 5th International Workshop on Automated Specification and Verification of Web Systems (WWV'09). 2009. [bib]
[BW09] B. Beckert and M. Wagner. Probabilistic Models for the Verification of Human-Computer Interaction. In Proc. 32nd Annual German Conference on Artificial Intelligence. 2009. [bib]
[BLMS09] R. Barbuti, F. Levi, P. Milazzo and G. Scatena. Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates. In 3rd International Workshop on Reachability Problems (RP'09). 2009. [bib]
[BES09] D. Bosnacki and S. Edelkamp and D. Sulewski. Efficient Probabilistic Model Checking on General Purpose Graphics Processors. In C. Pasareanu (editor) Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 32-49, Springer. 2009. [bib]
[HHZ09] E. Hahn, H. Hermanns and L. Zhang. Probabilistic Reachability for Parametric Markov Models. In C. Pasareanu (editor) Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 88-106, Springer. 2009. [bib]
[BKPA09] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. Probabilistic model checking for the quantification of DoS security threats. Computers & Security, Elsevier. 2009. [bib]
[ACvdM+09] F. Arbab, T. Chothia, R. van der Mei, M. Sun, Y.-J. Moon and C. Verhoef. From Coordination to Stochastic Models of QoS. In Proc. 11th international conference on Coordination Models and Languages (Coordination'09). 2009. [bib]
[Ndu09] U. Ndukwu. Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems. In Proc. Workshop on Quantitative Formal Methods (QFM'09). 2009. [bib]
[DTC+09] A. Dhama, O. Theel, P. Crouzen, H. Hermanns, R. Wimmer and B. Becker. Dependability Engineering of Silent Self-stabilizing Systems. In Proc. 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems, volume 5873 of LNCS, pages 238-253, Springer. 2009. [bib]
[SM09] I. Saha and D. Mukhopadhyay. Quantitative Analysis of a Probabilistic Non-repudiation Protocol through Model Checking. In Proc. 5th International Conference on Information Systems Security (ICISS'09), volume 5905 of LNCS, pages 292-300, Springer. 2009. [bib]
[KH09a] M. Kattenbelt and M. Huth. Verification and Refutation of Probabilistic Specifications via Games. In Ravi Kannan and K Narayan Kumar (editors) Proc. 29th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), pages 251-262, LIPIcs. December 2009. [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]
[JKNT09] M. Jurdzinski, M. Kwiatkowska, G. Norman and A. Trivedi. Concavely-Priced Probabilistic Timed Automata. In M. Bravetti and G. Zavattaro (editors) Proc. 20th Int. Conf. Concurrency Theory (CONCUR'09), volume 5710 of LNCS, pages 415-430, 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]
[HH09] A. Hartmanns and H. Hermanns. A Modest Approach to Checking Probabilistic Timed Automata. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). To appear. September 2009. [bib]
[AMMKQ09] F. Arbab, S. Meng, Y.-J. Moon, M. Kwiatkowska and H. Qu. Reo2MC: a Tool Chain for Performance Analysis of Coordination Models. In Hans van Vliet, ValÃ©rie Issarny (editor) The 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 287-288, ACM. August 2009. [pdf] [bib]
[KH09b] M. Kwiatkowska and J. Heath. Biological pathways as communicating computer systems. Journal of Cell Science, 122(16), pages 2793-2800. August 2009. [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]
[Mai09] V. Maisonneuve. Automatic heuristic-based generation of MTBDD variable orderings for PRISM models. Internship report, ENS Cachan & Oxford University Computing Laboratory. July 2009. [pdf] [bib]
[CK09a] V. Issarny, B. Steffen, B. Jonsson, G. Blair, P. Grace, M. Kwiatkowska, R. Calinescu, P. Inverardi, M. Tivoli, A. Bertolino and A. Sabetta. CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems. In Proc. 14th IEEE International Conference on Engineering of Complex Computer Systems. Poster. June 2009. [pdf] [bib]
[Kwi09] M. Kwiatkowska. On Quantitative Software Verification. In C. Pasareanu (editor) Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 2-3, Springer. Invited contribution. June 2009. [pdf] [bib]
[Dwo09] H. Dworak. The Design and Implementation of a Documentation Generator for the PRISM Language. In Proc. 4th International Conference on Dependability of Computer Systems (DepCoS-RELCOMEX'09), pages 91-98, IEEE Computer Society. June 2009. [bib]
[CK09] R. Calinescu and M. Kwiatkowska. Using Quantitative Analysis to Implement Autonomic IT Systems. In Proc. 31st International Conference on Software Engineering (ICSE 2009), pages 100-110, IEEE Press. May 2009. [pdf] [bib]
[BG+09] M. ter Beek, S. Gnesi, D. Latella, M. Massink, M. Sebastianis and G. Trentanni. Assisting the Design of a Groupware System - Model Checking Usability Aspects of thinkteam. Journal of Logic and Algebraic Programming, 78(4), pages 191-232, Elsevier. April 2009. [bib]
[CK09b] R. Calinescu and M. Kwiatkowska. CADS*: Computer-Aided Development of Self-* Systems. In Marsha Chechik and Martin Wirsing (editors) Fundamental Approaches to Software Engineering (FASE 2009), volume 5503 of Lecture Notes in Computer Science, pages 421-424, Springer-Verlag. March 2009. [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. March 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. 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. March 2009. [ps.gz] [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]

2008

[AGM08] D. Ardagna, C. Ghezzi and R. Mirandola. Model Driven QoS Analyses of Composed Web Services. In Proc. ServiceWave 2008, volume 5377 of LNCS, pages 299-311, Springer. 2008. [bib]
[ERE08] A. El Rayes and M. Er. Using the Probabilistic Model Checker PRISM to Analyze Credit Card Use. Electronic Journal of Information Systems Evaluation, 11(1). 2008. [bib]
[BKPA08] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. A Probabilistic Attacker Model for Quantitative Verification of DoS Security Threats. In Proc. 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'08), pages 12-19, IEEE CS Press. 2008. [bib]
[GGMT08] S. Gallotti, C. Ghezzi, R. Mirandola and G. Tamburrelli. Quality Prediction of Service Compositions through Probabilistic Model Checking. In Proc. 4th International Conference on the Quality of Software-Architectures (QoSA'08), volume 5281 of LNCS, pages 119-134, Springer. 2008. [bib]
[Ma08] Zhongdan Ma. Modelling with PRISM of Intelligent System. Masters thesis, University of Oxford. 2008. [pdf] [bib]
[CH09] F. Ciocchetta and J. Hillston. Bio-PEPA for epidemiological models. In Proc. 4th International Workshop on Practical Applications of Stochastic Modelling (PASM'09). 2008. [bib]
[HGD08] M. Heiner, D. Gilbert and R. Donaldson. Petri Nets for Systems and Synthetic Biology. In Formal Methods for Computational Systems Biology, volume 5016 of LNCS, pages 215-264, Springer. 2008. [bib]
[OTGT08] N. Owens, J. Timmis, A. Greensted and A. Tyrrell. Modelling the Tunability of Early T Cell Signalling Events. In 7th International Conference on Artificial Immune Systems (ICARIS'08), pages 12-23. 2008. [bib]
[EKVY08] K. Etessami, M. Kwiatkowska, M. Vardi and M. Yannakakis. Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science, 4(4), pages 1-21. 2008. [pdf] [bib]
[SAA+08] A. Susu, A. Acquaviva, A. Atienza and and A. De Micheli. Stochastic Modeling and Analysis for Environmentally Powered Wireless Sensor Nodes. In Proc. 6th International Symposium on Modeling and Optimization in Mobile, Ad Hoc, and Wireless Networks (WiOPT'08), pages 11-20. 2008. [bib]
[BPdV08] D. Bosnacki, T. Pronk and E. de Vink. In Silico Modelling and Analysis of Ribosome Kinetics and aa-tRNA Competition. In R.-J. Back and I. Petre (editors) Proc. Workshop on Computational Models for Cell Processes (COMPMOD'08), pages 23-38. 2008. [bib]
[WS08] F. Werner and P. Schmitt. Analysis of the Authenticated Query Flooding Protocol by Probabilistic Means. In Proc. 5th Annual Conference on Wireless On demand Network Systems and Services (WONS'08), pages 101-104. 2008. [bib]
[CT08] A. Coker and V. Taylor. Performance and Reliability Analysis of a Scaled Multi-Switch Junction Crossbar Nanomemory and Demultiplexer. In Proc. IEEE NANO Conference. 2008. [bib]
[CGGH08] F. Ciocchetta, S. Gilmore, M. L. Guerriero and J. Hillston. Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems. In Proc. 3rd International Workshop on Practical Applications of Stochastic Modelling (PASM'08), volume 232 of ENTCS, pages 17-38. 2008. [bib]
[ZHHW08] L. Zhang, H. Hermanns, E. M. Hahn and B. Wachter. Time-bounded model checking of infinite-state continuous-time Markov chains. In Proc. 8th International Conference on Application of Concurrency to System Design (ACSD'08), pages 98-107. 2008. [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]
[ENT08] J. Elmqvist and S. Nadjm-Tehrani. Formal Support for Quantitative Analysis of Residual Risks in Safety-Critical Systems. In Proc. High Assurance Systems Engineering Symposium (HASE'08). December 2008. [bib]
[CK08] R. Calinescu and M. Kwiatkowska. Software Engineering Techniques for the Development of Systems of Systems. In Proc. 15th Monterey Workshop on Foundations of Computer Software, pages 86--93. September 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]
[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]
[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]
[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. February 2008. [ps.gz] [pdf] [bib]
[SDM08] A. Sesic, S. Dautovic and V. Malbasa. Dynamic Power Management of a System With a Two-Priority Request Queue Using Probabilistic-Model Checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(2). February 2008. [bib]
[Sch08] O. Schaeffer. On the use of process algebra techniques in computational modelling of cancer initiation and development. Ph.D. thesis, University of Birmingham. February 2008. [pdf] [bib]
[KKNP08c] M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker. A Game-based Abstraction-Refinement Framework for Markov Decision Processes. Technical report RR-08-06, Oxford University Computing Laboratory. 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. [bib]

2007

[BGRC+07] F. Bernardini, M. Gheorghe, F. Romero-Campero and N. Walkinshaw. A Hybrid Approach to Modelling Biological Systems. In Proc. 8th Workshop on Membrane Computing, volume 4860 of Lecture Notes in Computer Science, Springer. 2007. [bib]
[HBGS07] F. He, L. Baresi, C. Ghezzi and P. Spoletini. Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata. In Proc. Formal Techniques for Networked and Distributed Systems (FORTE'07), volume 4574 of Lecture Notes in Computer Science, pages 247-262, Springer. 2007. [bib]
[CGW07] R. Colvin, L. Grunske and K. Winter. Probabilistic Timed Behavior Trees. In Proc. 6th International Conference on Integrated Formal Methods (IFM'07). 2007. [bib]
[GHL07] D. Gilbert, M. Heiner and S. Lehrack. A Unifying Framework for Modelling and Analysing Biochemical Pathways Using Petri Nets. In Proc. 5th International Conference on Computational Methods in Systems Biology (CMSB'07), pages 200-216, Springer. 2007. [bib]
[Kal07] E. Kaldeli. Investigating formal representations of PIN block attacks. Masters thesis, School of Informatics, University of Edinburgh. 2007. [bib]
[JKO+07] D. Jansen, J.-P. Katoen, M. Oldenkamp, M. Stoelinga and I. Zapreev. How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In Haifa Verification Conference 2007, pages 69-85. 2007. [bib]
[DAp07] D. D'Aprile. Timed and Stochastic Model Checking of Petri Nets. Ph.D. thesis, Dipartimento di Informatica, University of Torino. 2007. [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]
[STKT07] T. Sekizawa, T. Tsuchiya, T. Kikuno, and K. Takahashi. Analyzing the One Dimensional Ising Model by Probabilistic Model Checking. In Proc. IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007). To appear. October 2007.
[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]
[LJ07] C. Langmead and S. Jha. Predicting Protein Folding Kinetics Via Temporal Logic Model Checking. In 7th International Workshop on Algorithms in Bioinformatics (WABI'07), volume 4645 of Lecture Notes in Computer Science, pages 252-264, Springer. September 2007. [bib]
[Kwi07] M. Kwiatkowska. Quantitative Verification: Models, Techniques and Tools. In Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 449-458, ACM Press. September 2007. [pdf] [bib]
[GCW07] L. Grunske, R. Colvin and K. Winter. Probabilistic Model-Checking Support for FMEA. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07). September 2007. [bib]
[RSPV07] V. Rosset, P. Souto, P. Portugal and F. Vasques. A Reliability Evaluation of a Group Membership Protocol. In Proc. SAFECOMP 2007, volume 4680 of LNCS, pages 397-410, Springer. September 2007. [bib]
[WZH07] B. Wachter, L. Zhang and H. Hermanns. Probabilistic Model Checking Modulo Theories. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07). September 2007. [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]
[KNSW07] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007. [ps.gz] [pdf] [bib]
[Vys07] V. Vyshemirsky. Probabilistic Reasoning and Inference for Systems Biology. Ph.D. thesis, University of Glasgow. July 2007. [bib]
[FMM07] A. Fehnker, M. Fruth and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. In Proc. Workshop on Methods, Models and Tools for Fault-Tolerance (MeMoT'07) at the 7th International Conference on Integrated Formal Methods (IFM'07), pages 80-87. Technical Report CS-TR-1032, University of Newcastle upon Tyne. July 2007. [pdf] [bib]
[PVBB07] T. Pronk, E. de Vink, D. Bosnacki and T. Breit. Stochastic Modeling of Codon Bias with PRISM. In I. Linden and C. Talcott (editors) Proc. MTCoord 2007, Paphos, Computer Science Department, University of Cyprus, Nicosia. June 2007. [bib]
[GF07a] J. Greifeneder and J. Frey. Probabilistic Timed Automata for Modeling Networked Automation Systems. In Proc. 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS), pages 143-148. June 2007. [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. [ps.gz] [pdf] [bib]
[EKVY07] K. Etessami, M. Kwiatkowska, M. Vardi and M. Yannakakis. Multi-Objective Model Checking of Markov Decision Processes. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 50-65, Springer. March 2007. [pdf] [bib]
[KKZJ07] J.-P. Katoen, T. Kemna, I. Zapreev and D. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 87-101, Springer. March 2007. [bib]
[Der07] S. Derisavi. A Symbolic Algorithm for Optimal Markov Chain Lumping. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 139-154, Springer. March 2007. [bib]
[RBB07] G. Roelke, R. Baldwin and D. Bulutoglu. Analytical Models for the Performance of von Neumann Multiplexing. IEEE Transactions on Nanotechnology, 6(1), pages 75-89. January 2007. [bib]
[SMA+07] A. Susu, M. Magno, A. Acquaviva, D, Atienzay and G. De Micheli. Reconfiguration Strategies for Environmentally Powered Devices: Theoretical Analysis and Experimental Validation. Transactions on High-Performance Embedded Architectures and Compilers, 1(1), pages 327-346. January 2007. [bib]

2006

[Che06] L. Cheung. Reconciling Nondeterministic and Probabilistic Choices. Ph.D. thesis, Radboud University of Nijmegen. 2006. [bib]
[Tro06] A. Troina. Probabilistic Timed Automata for Security Analysis and Design. Ph.D. thesis, University of Pisa. 2006.
[CVGO06] M. Calder, V. Vyshemirsky, D. Gilbert and R. Orton. Analysis of signalling pathways using continuous time Markov chains. Transactions on Computational Systems Biology VI, 4220, pages 44-67, Springer. 2006. [bib]
[Ste06] G. Steel. Formal Analysis of PIN Block Attacks. Theoretical Computer Science, 367(1-2), pages 257-270, Elsevier. 2006. [bib]
[Adi06] M. Adithia. Probabilistic Analysis of Network Anonymity using PRISM. Masters thesis, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven. 2006. [bib]
[CDDS06] D. Cerotti, D. D'Aprile, S. Donatelli and J. Sproston. Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools. In Proc. 6th International Conference on Application of Concurrency to System Design (ACSD'06), IEEE Computer Society Press. 2006. [bib]
[FP06] W. Fokkink and J. Pang. Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM. Journal of Universal Computer Science, 12(8), pages 981--1006. 2006. [bib]
[DIM+06] G. Della Penna, B. Intrigila, I. Melatti, E. Tronci and M. Venturini Zilli. Finite Horizon Analysis of Markov Chains with the Murphi Verifier. International Journal on Software Tools for Technology Transfer (STTT), 8(4-5), pages 397-409, Springer. 2006. [bib]
[CB06] D. Chu and I. Blomfield. Orientational control is an efficient control mechanism for phase switching in the E.coli fim system. Journal of Theoretical Biology, Elsevier. To appear. 2006. [bib]
[BSGG06] D. Bhaduri, S. Shukla, P. Graham and M. Gokhale. Comparing Reliability-Redundancy Trade-offs for Two Von Neumann Multiplexing Architectures. IEEE Transactions on Nanotechnology. To appear. 2006.
[McI06] A. McIver. Quantitative refinement and model checking for the analysis of probabilistic systems. In Proc. Formal Methods (FM'06). To appear. 2006. [bib]
[FG06] A. Fehnker and P. Gao. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In Proc. 5th International Conference on Ad-Hoc, Mobile, and Wireless Networks (ADHOC-NOW'06), volume 4104 of LNCS, pages 128-141, Springer. 2006. [bib]
[SUH+06] H. Sauro, A. Uhrmacher, D. Harel, M. Hucka, M. Kwiatkowska, P. Mendes, C. Shaffer, L. Stromback and J. Tyson. Challenges for modeling and simulation methods in systems biology. In L. Perrone, F. Wieland, J. Liu, B. Lawson, D. Nicol and R. Fujimoto (editors) Proc. 2006 Winter Simulation Conference, pages 1720-1730, IEEE. December 2006. [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 L. F. Perrone, F. P. Wieland, J. Liu, B. G. Lawson, D. M. Nicol, and R. M. Fujimoto (editors) Proceedings of the 2006 Winter Simulation Conference, pages 1666-1674, Winter Simulation Conference. December 2006. [ps.gz] [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]
[NS06] G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. Journal of Computer Security, 14(6), pages 561-589, IOS Press. November 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]
[Fru06] M. Fruth. Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network Protocol. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'06). November 2006. [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]
[DM06] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Model Checking using Generic Representatives. In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of LNCS, pages 9-23, Springer. October 2006. [bib]
[GF06d] J. Greifeneder and J. Frey. Probabilistic Hybrid Automata with Variable Step Width Applied to the Analysis of Networked Automation Systems. In Proc. 3rd IFAC Workshop on Discrete Event System Design (DESDes'06), pages 283-288. September 2006. [bib]
[GF06c] J. Greifeneder and J. Frey. Optimizing Quality of Control in Networked Automation Systems using Probabilistic Models. In Proc. 11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'06), pages 372-379. September 2006. [bib]
[Wan06] F. Wang. Symbolic Implementation of Model-Checking Probabilistic Timed Automata. Ph.D. thesis, University of Birmingham. September 2006. [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]
[Kem06] T. Kemna. Bisimulation Minimisation and Probabilistic Model Checking. Masters thesis, University of Twente. August 2006. [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]
[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]
[GF06b] J. Greifeneder and G. Frey. Determination of Delay Times in Failure Afflicted Networked Automation Systems using Probabilistic Model Checking. In Proc. 6th IEEE International Workshop on Factory Communication Systems (WFCS'06), pages 263-272. June 2006. [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), Springer. 216-228. June 2006. [ps.gz] [pdf] [bib]
[GF06] J. Greifeneder and G. Frey. Dependability analysis of networked automation systems by probabilistic delay time analysis. In Proc. 12th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'06), pages 269-274. May 2006. [bib]
[GRV06] U. Glasser, S. Rastkar and M. Vajihollahi. Computational Modeling and Experimental Validation of Aviation Security Procedures. In Proc. Intelligence and Security Informatics (ISI'06) . May 2006.
[ZH06] M. Zhang and D. Van Hung. Formal Analysis of Streaming Downloading Protocol for System Upgrading. In Proc. 4th Workshop on Quantitative Aspects of Programming Languages (QAPL 06). Also available as UNU-IIST Report No. 332. April 2006. [bib]
[BCS+06] D. Bhaduri, S. Shukla, D. Coker, V. Taylor, P. Graham and M. Gokhale. A Hybrid Framework for Design and Analysis of Fault Tolerant Architectures and its Applications to Nanoscale Molecular Crossbar Memories. In Proc. Design, Automation and Test in Europe (DATE'06). March 2006.
[LS06] K. Lampka and M. Siegle. Activity-Local Symbolic State Graph Generation for High-Level Stochastic Models. In Proc. 13th GI/ITG Conference on Measuring, Modelling and Evaluation of Computer and Communication Systems (MMB), pages 245-263. March 2006. [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]
[BFW06] P. Ballarini, M. Fisher and M. Wooldridge. Automated Game Analysis via Probabilistic Model Checking: A Case Study. In Proc. 3rd Workshop on Model Checking and Artificial Intelligence (MoChArt'05), volume 149 of ENTCS, pages 125-137, Elsevier. February 2006. [bib]
[KNP06e] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. Computers & Mathematics with Applications, 51(2), pages 305-316, Elsevier. January 2006. [ps.gz] [pdf] [bib]

2005

[MM05b] A. McIver and C. Morgan. Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic. To appear. 2005. [bib]
[GB05] N. Geisweiller and J. Bonte. Performance Evaluation of a Real-time Simulation Architecture using Probabilistic Model Checking. In Proc. Workshop on Structural Operational Semantics (SOS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 3-24. 2005. [bib]
[Che05] L. Cheung. Randomized Wait-Free Consensus using An Atomicity Assumption. In Proc. 9th International Conference on Principles of Distributed Systems (OPODIS'05). Full version available as Technical Report ICIS-R05035, Institute for Computing and Information Sciences, Radboud University Nijmegen. November 2005. [bib]
[Hec05] R. Heckel. Stochastic Analysis of Graph Transformation Systems: A Case Study in P2P Networks. In Proc. 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC'05), volume 3722 of LNCS, Springer. October 2005.
[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]
[WK05] F. Wang and M. Kwiatkowska. An MTBDD-based implementation of forward reachability for probabilistic timed automata. In Proc. 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 385-399, Springer. 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]
[Hil05] J. Hillston. Fluid Flow Approximation of PEPA Models. In Proc. 2nd International Conference on Quantitative Evaluation of Systems (QEST'05), pages 33-42, IEEE CS Press. September 2005. [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]
[Bal05] P. Ballarini. Automated Game Analysis via Probabilistic Model Checking. In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS'05), pages 15-18. September 2005. [bib]
[GF05] J. Greifeneder and G. Frey. Probabilistic Delay Time Analysis in Networked Automation Systems. In Proc. 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'05), pages 1065-1068. September 2005. [bib]
[BP05] M. Bhargava and C. Palamidessi. Probabilistic Anonymity. In Proc. 16th International Conference on Concurrency Theory (CONCUR'05). August 2005. [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]
[DPP05] Y. Deng, C. Palamidessi and J. Pang. Weak Probabilistic Anonymity. In Proc. 3rd International Workshop on Security Issues in Concurrency (SecCo'05). August 2005. [bib]
[BCM+05] R. Barbuti, S. Cataudella, A. Maggiolo-Schettini, P. Milazzo and A. Troina. A Probabilistic Model for Molecular Systems. Fundamenta Informaticae, 67(1-3), pages 13-27. July 2005. [bib]
[You05] H. Younes. Ymer: A Statistical Model Checker. In Proc. 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 429-433, Springer-Verlag. July 2005. [bib]
[BML05b] M. ter Beek, M. Massink and D. Latella. Towards Model Checking Stochastic Aspects of the thinkteam User Interface. In M. Harrison (editor) Proc. 12th International Workshop on Design, Specification and Verification of Interactive Systems (DSVIS'05), volume 3941 of Lecture Notes in Computer Science, pages 39-50, Springer. July 2005. [bib]
[DM05] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Systems. In Proc. 12th workshop on Automated Reasoning, pages 17-18. July 2005. [bib]
[RG05] A. Roy and K. Gopinath. Improved Probabilistic Models for 802.11 Protocol Verification. In Proc. 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 239-252, Springer-Verlag. July 2005. [bib]
[GK05] S. Gilmore and L. Kloul. A Unified Tool for Performance Modelling and Prediction. Reliability Engineering and System Safety, 89(1), pages 17-32, Elsevier. To appear. July 2005.
[GW05] M. Goldsmith and P. Whittaker. A CSP Frontend for Probabilistic Tools. Technical report FORWARD Deliverable D14, Formal Systems (Europe Ltd). June 2005. [bib]
[CKKP05] L. Cloth, J.-P. Katoen, M. Khattri and R. Pulungan. Model checking Markov reward models with impulse rewards. In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 722-731, IEEE CS Press. June 2005. [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]
[GNP05] S. Gay, R. Nagarajan and N. Papanikolaou. Probabilistic Model Checking of Quantum Protocols. Quantum Physics Repository article quant-ph/0504007. April 2005.
[MM05a] A. McIver and C. Morgan. An elementary proof that Herman's Ring is THETA(N-squared). Information Processing Letters, 94(2), pages 79-84. April 2005. [bib]
[Hin05] A. Hinton. Software Project M60: Simulator for the Probabilistic Model Checker PRISM. MEng Final Year Project Dissertation, School of Computer Science, University of Birmingham. April 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]
[CVGO05] M. Calder, V. Vyshemirsky, D. Gilbert and R. Orton. Analysis of signalling pathways using the PRISM model checker. In Proc. Computational Methods in Systems Biology (CMSB'05), pages 179-190. 2005. [bib]
[ISSG05] S. Irani, G. Singh, S. Shukla and R. Gupta. An Overview of the Competitive and Adversarial Approaches to Designing Dynamic Power Management Strategies. IEEE Transactions on VLSI Systems. 2005. [bib]
[BML05a] M. ter Beek, M. Massink, and D. Latella. Towards Model Checking Stochastic Aspects of the thinkteam User Interface - FULL VERSION. Technical report 2005-TR-18, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche. 2005. [bib]
[NPBG05] R. Nagarajan, N. Papanikolaou, G. Bowen and S. Gay. An Automated Analysis of the Security of Quantum Key Distribution. In Proc. 3rd International Workshop on Security Issues in Concurrency (SecCo'05). 2005. [bib]

2004

[BCM+04] R. Barbuti, S. Cataudella, A. Maggiolo-Schettini, P. Milazzo and A. Troina. A Probabilistic Calculus for Molecular Systems. In Proc. Concurrency Specification and Programming (CS&P'04). 2004. [bib]
[KSW04b] M. Kuntz, M. Siegle and E. Werner. CASPA: A Tool for Symbolic Performance and Dependability Evaluation. In Supplemental Volume of Proc. of Int. Conf. on Dependable Systems and Networks (DSN'04), pages 90-91. 2004.
[Shm04] V. Shmatikov. Probabilistic Model Checking of an Anonymity System. Journal of Computer Security, 12(3/4), pages 355-377. 2004. [bib]
[KSW04a] M. Kuntz, M. Siegle and E. Werner. Symbolic Performance and Dependability Evaluation with the Tool CASPA. In Proc. 1st European Performance Engineering Workshop (EPEW'04), FORTE'04 workshop, volume 3236 of LNCS, pages 293-307, Springer-Verlag. 2004. [bib]
[Gol04] M. Goldsmith. CSP: The Best Concurrent-System Description Language in the World - Probably!. In Proc. Communicating Process Architectures (CPA'04). 2004. [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]
[DIM+04] G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, M. Venturini Zilli. Bounded Probabilistic Model Checking with the Murphi Verifier. In Proc. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of LNCS, pages 214-229, Springer-Verlag. November 2004.
[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]
[Meh04b] R. Mehmood. Disk-based techniques for efficient solution of large Markov chains. Ph.D. thesis, University of Birmingham. October 2004. [ps.gz] [pdf] [bib]
[Nor04] G. Norman. Analysing Randomized Distributed Algorithms. 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 384--418, Springer. October 2004. [ps.gz] [pdf] [bib]
[GHHK04] S. Gilmore, V. Haenel, J. Hillston and L. Kloul. PEPA nets in practice: Modelling a decentralised peer-to-peer emergency medical application. In Proc. 1st European Performance Evaluation Workshop (EPEW'04), volume 3236 of LNCS, pages 262-277, Springer-Verlag. October 2004.
[HLM04] R. Heckel, G. Lajios and S. Menge. Stochastic Graph Transformation Systems. In Proc. 2nd International Conference on Graph Transformations (ICGT'04), volume 3256 of LNCS, pages 210-225, Springer. October 2004. [bib]
[KNSW04] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. In Y. Lakhnech and S. Yovine (editors) Proc. FORMATS/FTRTFT'04, volume 3253 of Lecture Notes in Computer Science, pages 293-308, Springer. 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]
[FP04] W. Fokkink and J. Pang. Simplifying Itai-Rodeh leader election for anonymous rings. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 53-68, Elsevier Science. September 2004. [bib]
[DFH+04] M. Duflot, L. Fribourg, T. HÃ©rault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet and C. Picaronny. Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 195-214, Elsevier Science. September 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]
[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. August 2004. [ps.gz] [pdf] [bib]
[Meh04a] R. Mehmood. Serial Disk-based Analysis of Large Stochastic Models. 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, Springer-Verlag. August 2004. [ps.gz] [pdf] [bib]
[DSS04] R. Dingledine, V. Shmatikov and P. Syverson. Synchronous Batching: From Cascades to Free Routes. In Proc. 4th Workshop on Privacy Enhancing Technologies (PET). May 2004. [bib]
[BS04] D. Bhaduri and S. Shukla. NANOPRISM: A Tool for Evaluating Granularity vs. Reliability Trade-offs in Nano Architectures. In Proc. 14th Great Lakes Symposium on VLSI (GLSVLSI'04), ACM. April 2004.
[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), 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]
[DKN04] C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5(2), pages 221-236. March 2004. [ps.gz] [pdf] [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]
[LMST04] R. Lanotte, A. Maggiolo-Schettini and A. Troina. Automatic Analysis of a Non-Repudiation Protocol. In Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04). March 2004. [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]
[HLMP04] T. Herault, R. Lassaigne, F. Magniette and S. Peyronnet. Approximate Probabilistic Model Checking. In Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), volume 2937 of Lecture Notes in Computer Science, Springer-Verlag. January 2004. [bib]
[DDS04] D. D'Aprile, S. Donatelli and J. Sproston. CSL Model Checking for the GreatSPN Tool. In C. Aykanat, T. Dayar and I. Korpeoglu (editors) International Symposium on Computer and Information Sciences, volume 3280 of Lecture Notes in Computer Science, pages 543-552, Springer Verlag. 2004.
[Pap04] N. Papanikolaou. Techniques for Design and Validation of Quantum Protocols. Masters thesis, Department of Computer Science, University of Warwick. 2004.

2003

[GHB+03] M. Gribaudo, A. Horvath, A. Bobbio, E. Tronci, E. Ciancamerla and M. Minichino. Fluid Petri Nets and Hybrid Model-checking: A Comparative Case Study. Reliability Engineering and System Safety, 81, pages 239-257. 2003. [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]
[BDGK03] J. Bradley, N. Dingle, S. Gilmore and W. Knottenbelt. Derivation of passage-time densities in PEPA models using IPC: The Imperial PEPA Compiler. In Proc. 11th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunications Systems (MASCOTS'03), pages 344-351. October 2003.
[DIM+03a] G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, M. Venturini Zilli. Finite Horizon Analysis of Markov Chains with the Murphi Verifier. In Proc. 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), volume 2860 of LNCS, pages 394-409, Springer-Verlag. October 2003. [bib]
[DIM+03b] G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, M. Venturini Zilli. Finite Horizon Analysis of Stochastic Systems with the Murphi Verifier. In Proc. 8th Italian Conference on Theoretical Computer Science (ICTCS'03), volume 2841 of LNCS, Springer-Verlag. October 2003. [bib]
[Jan03] D. Jansen. Extensions of statecharts with probability, time, and stochastic timing. Ph.D. thesis, Universiteit Twente. October 2003.
[KNS03d] M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Model Checking for Probabilistic Timed Automata. Technical report CSR-03-10, School of Computer Science, University of Birmingham. October 2003. [ps.gz] [pdf] [bib]
[GK03] S. Gilmore and L. Kloul. A unified tool for performance modelling and predicition. In Proc. 22nd International Conference on Computer Safety, Reliability and Security (SAFECOMP'03), volume 2788 of LNCS, pages 179-192, Springer-Verlag. September 2003.
[JPS03] J. Jayaputera, I. Poernomo, H. Schmidt. Timed Probabilistic Reasoning on UML Specialization for Fault Tolerant Component Based Architectures. In Proc. Specification and Verification of Component-Based Systems (SAVCBS'03), Workshop at ESEC/FSE'03. September 2003.
[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). 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]
[Kwi03] M. Kwiatkowska. Model Checking for Probability and Time: From Theory to Practice. In Proc. 18th IEEE Symposium on Logic in Computer Science (LICS'03), pages 351-360, IEEE CS Press. Invited paper. June 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]
[GHKR03] S. Gilmore, J. Hillston, L. Kloul and M. Ribaudo. Performance modelling with PEPA nets and PRISM. In Proc. 2nd Workshop on Process Algebra and Stochastically Timed Activities (PASTA Secondi Piatti), pages 23-39. June 2003.
[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]
[KNS03b] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol. Formal Aspects of Computing, 14(3), pages 295-318. April 2003. [ps.gz] [pdf] [bib]

2002

[NS02] G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. In A. Abdallah, P. Ryan and S. Schneider (editors) Proc. BCS-FACS Formal Aspects of Security (FASec'02), volume 2629 of Lecture Notes in Computer Science, pages 81-96, Springer. December 2002. [ps.gz] [pdf] [bib]
[KN02] M. Kwiatkowska and G. Norman. Verifying Randomized Byzantine Agreement. In D. Peled and M. Vardi (editors) Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 194-209, Springer. November 2002. [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]
[JHK02] D. Jansen, H. Hermanns and J.-P. Katoen. A Probabilistic Extension of UML Statecharts Specification and Verification. In Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 355-374, Springer-Verlag. September 2002.
[KNP02d] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. In Proc. 2nd Euro-Japanese Workshop on Stochastic Risk Modelling for Finance, Insurance, Production and Reliability. September 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]
[KNS02a] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In H. Hermanns and R. Segala (editors) Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 169-187, Springer. July 2002. [ps.gz] [pdf] [bib]
[KM02] M. Kwiatkowska and R. Mehmood. Out-of-Core Solution of Large Linear Systems of Equations arising from Stochastic Modelling. In Proc. PAPM/PROBMIV'02, volume 2399 of LNCS, pages 135-151, Springer-Verlag. July 2002. [ps.gz] [bib]
[DKN02] C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. In Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), volume 66.2 of ENTCS. July 2002. [ps.gz] [pdf] [bib]
[KNP02c] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking CSL Until Formulae with Random Time Bounds. In H. Hermanns and R. Segala (editors) Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 152-168, Springer. July 2002. [ps.gz] [pdf] [bib]
[KNSS02] M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science, 282, pages 101-150. June 2002. [ps.gz] [pdf] [bib]
[Shm02] V. Shmatikov. Probabilistic Analysis of Anonymity. In Proc. 15th IEEE Computer Security Foundations Workshop (CSFW'02), pages 119-128, IEEE CS Press. June 2002. [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]
[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]

2001

[Spr01] J. Sproston. Model Checking for Probabilistic Timed and Hybrid Systems. Ph.D. thesis, School of Computer Science, The University of Birmingham. 2001. [ps.gz] [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]
[KNS01b] M. Kwiatkowska, G. Norman and J. Sproston. Symbolic computation of maximal probabilistic reachability. In K. Larsen and M. Nielsen (editors) Proc. 13th International Conference on Concurrency Theory (CONCUR'01), volume 2154 of LNCS, pages 169--183, Springer. August 2001. [ps.gz] [pdf] [bib]
[KNS01a] M. Kwiatkowska, G. Norman and R. Segala. Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM. In G. Berry, H. Common and A. Finkel (editors) Proc. CAV'01, volume 2102 of Lecture Notes in Computer Science, pages 194-206, Springer. January 2001. [ps.gz] [pdf] [bib]

2000

[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]

1999

[KNPS99] M. Kwiatkowska, G. Norman, D. Parker and R. Segala. Symbolic Model Checking of Concurrent Probabilistic Systems using MTBDDs and Simplex. Technical report CSR-99-01, School of Computer Science, University of Birmingham. January 1999. [ps.gz] [pdf] [bib]