PRISM Bibliography

The following is a bibliography of PRISM-related papers. This includes both papers from the PRISM team and from elsewhere.

See also the separate lists of PRISM-related papers produced externally and by the PRISM team, and the list of selected PRISM papers.

If there is something we have omitted, please contact us.

Sort by: date, type, title, subject

Case studies using PRISM
Underlying techniques in PRISM
Extensions and adaptions to PRISM
Tool/language connections to PRISM
PRISM tool papers
PRISM-related tutorials and surveys

596 publications:

Case studies using PRISM

2020

[TH20] Iram Tariq Bhatti and Osman Hasan. Formal Verification of a Fully Automated Out-of-Plane Cell Injection System. In Proc. 21st International Symposium on Quality Electronic Design (ISQED'20), pages 111-116. 2020. [Uses probabilistic model checking and PRISM to analyse the functional correctness and performance of a fully automated out-of-plane cell injection system.]
[MACD20] Nabor C. Mendonça, Carlos Mendes Aderaldo, Javier Cámara and David Garlan. Model-Based Analysis of Microservice Resiliency Patterns. In Proc. IEEE International Conference on Software Architecture (ICSA'20). 2020. [Uses PRISM to model and analyse the behaviour of two popular microservice resiliency patterns: Retry and Circuit Breaker.]

2019

[BBH+19] Nathalie Bertrand, Benjamin Bordais, Loïc Hélouët, Thomas Mari, Julie Parreaux and Ocan Sankur. Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking. In Proc. 3rd International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail'19), Springer. 2019. [Uses probabilistic model checking and PRISM to formally evaluate the performance of regulation algorithms in metro train lines.]
[SKII19] Khayyam Salehi, Jaber Karimpour, Habib Izadkhah and Ayaz Isazadeh. Channel Capacity of Concurrent Probabilistic Programs. Entropy, 21(9). 2019. [Studies information leakage for concurrent probabilistic programs using an extension of PRISM.]
[UAU+19] Riaz Uddin, Ali S. Alghamdi, Muhammad Hammad Uddin, Ahmed Bilal Awan and Syed Atif Naseem. Ethernet-Based Fault Diagnosis and Control in Smart Grid: A Stochastic Analysis via Markovian Model Checking. Journal of Electrical Engineering & Technology. 2019. [Formally analyses the reliability of fault detection, isolation and supply restoration (FDIR), including use of PRISM.]
[HMP+19] Richard Henze, Chunyan Mu, Mate Puljiz, Nishanthan Kamaleson, Jan Huwald, John Haslegrave, Pietro Speroni di Fenizio, David Parker, Christopher Good, Jonathan E. Rowe, Bashar Ibrahim and Peter Dittrich. Multi-scale Stochastic Organization-oriented Coarse-graining Exemplified on the Human Mitotic Checkpoint. Scientific Reports, 9(1), pages 3902, Nature Research. March 2019. [pdf] [bib] [Analyses biological models at various levels of coarse graining with several different tools, including PRISM.]

2018

[MCDMR18] Giovanni Mazzeo, Luigi Coppolino, Salvatore D’Antonio, Claudio Mazzariello and Luigi Romano. SIL2 Assessment of an Active/Standby COTS-Based Safety-related System. Reliability Engineering & System Safety. 2018. [Proposes an approach to safety certification for Commercial-Off-The-Shelf (COTS) components using PRISM.]
[WBD+08] Matt Webster, Michael Breza, Clare Dixon, Michael Fisher and Julie McCann. Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks. In Proc. Automated Verification of Critical Systems 2018 (AVoCS'18) . 2018. [Verifies protocols for wireless sensor networks using probabilistic model checking and PRISM.]
[NF18] Mehran Alidoost Nia and Fathiyeh Faghih. Probabilistic Analysis of Self-Stabilizing Systems: A Case Study on a Mutual Exclusion Algorithm. In Proc. 2018 Real-Time and Embedded Systems and Technologies (RTEST'18), IEEE. 2018. [Uses PRISM to analyse and improve a mutual exclusion algorithm.]
[Sal18] Maria Salama. Architectural Stability Of Self-Adaptive Software Systems. Ph.D. thesis, University of Birmingham. 2018. [Studies architectural stability of self-adaptive software systems, including trade-off analysis using PRISM-games.]
[TMR18] Pedro J. Rivera Torres, E. I. Serrano Mercado and E. I. Serrano Mercado. Probabilistic Boolean Network Modeling of an Industrial Machine. Journal of Intelligent Manufacturing. 2018. [Uses Probabilistic Boolean Networks to model manufacturing processes, and analyses models using PRISM.]
[KML+18] Justus A. Kromer, Steffen Märcker, Steffen Lange, Christel Baier and Benjamin M. Friedrich. Decision making improves sperm chemotaxis in the presence of noise. Computational Biology, 14(4). 2018. [Uses probabilistic model checking and PRISM to study decision making in sperm chemotaxis.]
[EPB18] Alexandros Evangelidis, David Parker and Rami Bahsoon. Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. Future Generation Computer Systems, 87, pages 629-638, Elsevier. October 2018. [pdf] [bib] [Presents an approach for producing formal performance guarantees for cloud-based auto-scaling policies using PRISM.]

2017

[SCA+17] Gautham Nayak Seetanadi, Javier Cámara, Luis Almeida, Karl-Erik Årzén and Martina Maggio. Event-Driven Bandwidth Allocation with Formal Guarantees for Camera Networks. In Proc. 2017 IEEE Real-Time Systems Symposium (RTSS'17), pages 243-254. 2017. [Uses PRISM to verify a bandwidth allocation scheme for camera networks.]
[SH17] Muhammad Usama Sardar and Osman Hasan. Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems. In Proc. Models for Formal Analysis of Real Systems (MARS'17), pages 271-282. 2017. [Models and analyses robotic cell injection systems using PRISM.]
[ZBDL17] Xi Zheng, Matthew L. Bolton, Christopher Daly and Lu Feng. A Formal Human Reliability Analysis of a Community Pharmacy Dispensing Procedure. In Proc. Human Factors and Ergonomics Society 2017 Annual Meeting, pages 728-732. 2017. [Uses probabilistic model checking and PRISM to predict medication error rates and explore interventions in pharmacy dispensing procedures.]
[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.]

2016

[AH16] Mohammed Alabdullatif and Reiko Heckel. Graph Transformation Games for Negotiating Features. In Proc. Graphs as Models 2016. 2016. [Proposes a negotiation game for designing flexible business interactions, with an underlying analysis based on PRISM-games.]
[GEK16] Sotirios Gyftopoulos, Pavlos S. Efraimidis and Panagiotis Katsaros. Solving Influence Problems on the DeGroot Model with a Probabilistic Model Checking Tool. In Proc. 20th Pan-Hellenic Conference on Informatics (PCI'16). 2016. [Uses PRISM-games to analyse the DeGroot model of opinion diffusion and formation in social networks.]
[LK16] Morteza Lahijanian and Marta Kwiatkowska. Specification Revision for Markov Decision Processes with Optimal Trade-off. In Proc. 55th Conference on Decision and Control (CDC'16), pages 7411-7418. 2016. [pdf] [bib] [Presents techniques for techniques for analysing trade-offs between the probability of satisfying a specification and the cost of revising, using PRISM as an underlying multi-objective model checker.]
[BKdM+16] Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier and Sascha Wunderlich. Greener Bits: Formal Analysis of Demand Response. In Proc. 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), pages 323-339, Springer. 2016. [Develops formal techniques for managing demand response in power generation, including a probabilistic analysis using PRISM. ]
[GDH16] Paul Gainer, Clare Dixon and Ullrich Hustadt. Probabilistic Model Checking of Ant-Based Positionless Swarming. In Proc. Towards Autonomous Robotic Systems (TAROS'16). 2016. [Uses probabilistic model checking and PRISM to study control algorithms for robot swarms.]
[PLM16] Zhaoguang Peng, Yu Lu and Alice Miller. Uncertainty Analysis of Phased Mission Systems with Probabilistic Timed Automata. In Proc. 7th IEEE International Conference on Prognostics and Health Management (PHM'16). 2016. [Analyses phased mission requirements using probabilistic timed automata and PRISM.]
[SAH+16] Muhammad Usama Sardar, Nida Afaq, Khaza Anuarul Hoque, Taylor T. Johnson and Osman Hasan. Probabilistic Formal Verification of the SATS Concept of Operation. In Proc. 8th International Symposium on NASA Formal Methods (NFM'16), volume 9690 of LNCS, pages 191–205, Springer. 2016. [Presents a formal analysis of NASA's Small Aircraft Transportation System (SATS) technology using probabilistic model checking and PRISM.]
[AC16] Jose Ignacio Aizpurua and Victoria M. Catterson. ADEPS: A Methodology for Designing Prognostic Applications. In Proc. 3rd European Conference of the Prognostics and Health Management Society. 2016. [Proposes ADEPS (Assisted Design for Engineering Prognostic Systems), which uses PRISM as an underlying verification tool.]
[NGMK16] Athanasios Naskos, Anastasios Gounaris, Haralambos Mouratidis and Panagiotis Katsaros. Online analysis of security risks in elastic cloud applications using probabilistic model checking. IEEE Cloud Computing Magazine. 2016. [Analyses the trade-offs between security risks and performance in cloud computing systems using probabilistic model checking and PRISM.]
[TMSR16] Pedro J. Rivera Torres, Eileen I. Serrano Mercado, Orestes Llanes Santiago and Luis Anido Rifon. Modeling preventive maintenance of manufacturing processes with probabilistic Boolean networks with interventions. Journal of Intelligent Manufacturing, Springer. 2016. [Proposes techniques based on probabilistic Boolean networks to analyse manufacturing processes, and uses PRISM as an underlying tool.]

2015

[BK15] Benoit Barbot and Marta Kwiatkowska. On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets. In Proc. 36th International Conference on Application and Theory of Petri Nets and Concurrency. 2015. [pdf] [Uses probabilistic model checking and PRISM to analyse DNA molecular walkers modelled as stochastic Petri nets.]
[HZHC15] Kangli He, Min Zhang, Jia He and Yixiang Chen. Probabilistic Model Checking of Pipe Protocol. In Proc. 9th International Symposium on Theoretical Aspects of Software Engineering (TASE'15). 2015. [Analyses the Pipe application layer protocol using probabilistic timed automata and PRISM.]
[Fra15] Joao Miguel Costa Sousa Franco. Automated Reliability Prediction and Analysis from Software Architectures. Ph.D. thesis, University of Coimbra. 2015. [Proposes automated techniques for predicting the reliability of software architectures, including the use of PRISM for model analysis.]
[CFR+15] Sanjian Chen, Lu Feng, Michael R. Rickels, Amy Peleckis, Oleg Sokolsky and Insup Lee. A Data-Driven Behavior Modeling and Analysis Framework for Diabetic Patients on Insulin Pumps. In Proc. IEEE International Conference on Healthcare Informatics (ICHI'15). 2015. [Proposes a modelling and analysis framework for the usage of insulin pumps, and studies the resulting models using PRISM.]
[UC15] Jose Ignacio Aizpurua Unanue and Victoria M. Catterson. On the use of probabilistic model-checking for the verification of prognostics applications. In Proc. IEEE Seventh International Conference on Intelligent Computing and Information Systems (ICICIS'15). 2015. [Applies probabilistic model checking and PRISM to prognostic techniques aimed at estimating the remaining useful life of assets.]
[CCDR15] Giuseppe Cicotti, Luigi Coppolino, Salvatore D'Antonio and Luigi Romano. Runtime Model Checking for SLA Compliance Monitoring and QoS Prediction. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, 6(2). 2015. [Proposes a QoS prediction approach using PRISM and applied to a smart grid case study.]
[CC15] Giuseppe Cicotti and Antonio Coronato. Towards a Probabilistic Model Checking-based approach for Medical Device Risk Assessment. In Proc. IEEE International Workshop on Medical Measurement and Applications (MEMEA'15). 2015. [Uses probabilistic model checking and PRISM in a new approach for quantitative medical device risk assessment.]
[TMR15] Pedro J. Rivera-Torres, E.I. Serrano Mercado and Anido L. Rifon. Probabilistic Boolean network modeling and model checking as an approach for DFMEA for manufacturing systems. Journal of Intelligent Manufacturing, pages 1-21, Springer. 2015. [Uses probabilistic Boolean networks and PRISM to analyse automated manufacturing assembly processes.]
[ZWC+15] Conghua Zhou, Yong Wang, Meiling Cao, Jianqi Shi and Yang Liu. Formal Analysis of MAC in IEEE 802.11p with Probabilistic Model Checking. In Proc. International Symposium on Theoretical Aspects of Software Engineering (TASE'15), pages 55-62, IEEE. 2015. [Uses probabilistic model checking and PRISM to analyse 802.11p for vehicular ad-hoc networks.]
[RMT15] Arunkumar Ramaswamy, Bruno Monsuez and Adriana Tapus. Model-driven self-adaptation of robotics software using probabilistic approach. In Proc. 2015 European Conference on Mobile Robots (ECMR'15). 2015. [Uses PRISM as part of a framework for model-driven self-adaptation of robotics software.]
[FWHT15] Lu Feng, Clemens Wiltsche, Laura Humphrey and Ufuk Topcu. Controller Synthesis for Autonomous Systems Interacting with Human Operators. In Proc. International Conference on Cyber-Physical Systems (ICCPS'15), ACM. 2015. [pdf] [Uses PRISM and PRISM-games to synthesize control protocols for autonomous systems interacting with human operators.]
[CGSP15] Javier Cámara, David Garlan, Bradley Schmerl and Ashutosh Pandey. Optimal Planning for Architecture-Based Self-Adaptation Via Model Checking of Stochastic Games. In Proc. 30th ACM Symposium on Applied Computing (SAC'15), Dependable and Adaptive Distributed Systems (DADS) track. 2015. [Proposes techniques for architecture-based self-adapation using stochastic multi-player games and PRISM-games.]
[RGH15] Daniël Reijsbergen, Stephen Gilmore and Jane Hillston. Patch-based Modelling of City-centre Bus Movement with Phase-type Distributions. In Proc. 7th International Workshop on Practical Applications of Stochastic Modelling (PASM'14), volume 310 of ENTCS, pages 157-177. 2015. [Uses HyperStar and PRISM on a stochastic performance model of a public transportation network.]
[CMG15] Javier Cámara, Gabriel A. Moreno and David Garlan. Reasoning about Human Participation in Self-Adaptive Systems. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes a formal framework for reasoning about human involvement in self-adaptive systems, using PRISM-games as an underlying model checker.]
[ASBL+15] A. Aldini, J.-M. Seigneur, C. Ballester Lafuente, X. Titi and J. Guislain. Formal Modeling and Verification of Opportunity-enabled Risk Management. In Proc. Trustcom International Symposium on Recent Advances of Trust, IEEE. 2015. [Formally analyses the opportunity-enabled risk management (OPPRIM) security framework using probabilistic model checking and PRISM.]
[HMS15] Khaza Anuarul Hoque, Otmane Ait Mohamed and Yvon Savaria. Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking. In Proc. 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE'15), pages 1635-1640. 2015. [Studies reliability, availability and maintainability properties of satellite systems using probabilistic model checking and PRISM.]
[MCGS15] Gabriel A. Moreno, Javier Cámara, David Garlan and Bradley Schmerl. Proactive self-adaptation under uncertainty: a probabilistic model checking approach. In Proc. 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE'15), pages 1-12. 2015. [Uses PRISM to synthesise latency-aware adaptation strategies for self-adaptive systems.]
[GCSG15] Thomas Glazier, Javier Cámara, Bradley Schmerl and David Garlan. Analyzing Resilience Properties of Different Topologies of Collective Adaptive Systems. In Proc. 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops (SASOW'15), pages 55-60. 2015. [Uses PRISM-games to analyse the impact of communication topologies for collective adaptive systems defending against an external attack.]
[JKG15] Benjamin Johnson and Hadas Kress-Gazit. Analyzing and revising synthesized controllers for robots with sensing and actuation errors. International Journal of Robotics Research, 34(6), pages 816-832. 2015. [Uses probabilistic model checking and PRISM for the synthesis of verifiable robot controllers.]

2014

[SDC+14] Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry and Sanjit A. Seshia. Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior. In Proc. AAAI Spring Symposium on Formal Verification & Modeling in Human-Machine Systems. 2014. [Analyses formal probabilistic models of driver behaviour, constructed with PRISM.]
[SCG+14] Bradley Schmerl, Javier Cámara, Jeffrey Gennari, David Garlan, Paulo Casanova, Gabriel A. Moreno, Thomas J. Glazier and Jeffrey M. Barnes. Architecture-based self-protection: composing and reasoning about denial-of-service mitigations. In Proc. 2014 Symposium and Bootcamp on the Science of Security (HotSoS'14). 2014. [Proposes adaptive techniques for denial-of-service mitigation, including formal analysis of adaptation strategies using PRISM.]
[FYO14] Ling Fang, Yoriyuki Yamagata and Yutaka Oiwa. Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking. In Proc. 3rd International Workshop on Engineering Safety and Security Systems 2014 (ESSS'14), volume 150 of EPTCS, pages 35-49. 2014. [Uses probabilistic model checking and PRISM to analyse resilience strategies for micro processor units.]
[ZR14] Yang Zhao and Kristin Yvonne Rozier. Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems. In Proc. IEEE/ACM 2014 International Conference on Computer-Aided Design (ICCAD'14), IEEE/ACM. 2014. [bib] [Uses probabilistic model checking and PRISM to study safety properties of automated air traffic control systems.]
[Ald14] Alessandro Aldini. Saving Privacy in Trust-Based User-Centric Distributed Systems. In Proc. 8th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE'14), pages 76-81. 2014. [Analyses privacy, cost and trust trade-offs in user-centric distributed systems using PRISM.]
[CS14] Muffy Calder and Michele Sevegnani. Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Aspects of Computing, 26(3), pages 537-561. 2014. [Analyses a model of the 802.11 CSMA/CA RTS/CTS protocol, modelled in an extension of stochastic bigraphical reactive systems, and then imported into PRISM]
[SBN14] Pravati Swain, Purandar Bhaduri and Sukumar Nandi. Probabilistic model checking of IEEE 802.11 IBSS power save mode. International Journal of Wireless and Mobile Computing, 7(7), pages 465-474. 2014. [Uses probabilistic model checking and PRISM to analyse a power management algorithm for Independent Basic Service Set (IBSS) from the IEEE 802.11 standard for wireless local area networks.]
[CMG14] Javier Cámara, Gabriel A. Moreno and David Garlan. Stochastic Game Analysis and Latency Awareness for Proactive Self-Adaptation. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), pages 155-164, ACM. 2014. [Uses PRISM-games to analyse adaptation tactic latency in self-adaptive systems.]
[BCG14] Ludovica Luisa Vissat, Allan Clark and Stephen Gilmore. Finding optimal timetables for Edinburgh bus routes. In Proc. 7th International Workshop on Practical Applications of Stochastic Modelling (PASM'14). 2014. [Uses various techniques and tools, including PRISM, to analyse and optimise bus reliability.]
[SBWA14] Khalid Sultan, Jamal Bentahar, Wei Wan and Faisal Al-Saqqar. Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments. Expert Systems with Applications, 41(14), pages 6291-6304, Elsevier. 2014. [Proposes techniques for analysing probabilistic multi-agent systems, implemented using PRISM.]
[DKSS14] Tushar Deshpande, Panagiotis Katsaros, Scott Smolka and Scott Stoller. Stochastic Game-Based Analysis of the DNS Bandwidth Amplification Attack Using Probabilistic Model Checking. In Proc. 10th European Dependable Computing Conference (EDCC'14). 2014. [Analyses the DNS bandwidth amplification attack using a stochastic game model and PRISM-games.]
[HMST14] Khaza Anuarul Hoque, Otmane Ait Mohamed, Yvon Savaria and Claude Thibeault . Early Analysis of Soft Error Effects for Aerospace Applications Using Probabilistic Model Checking. Formal Techniques for Safety-Critical Systems Communications in Computer and Information Science, 419, pages 54-70, Springer. 2014. [Uses probabilistic model checking and PRISM to analyse dependability and performability properties of SRAM-based FPGAs.]
[HMST14b] Khaza Anuarul Hoque, Otmane Ait Mohamed, Yvon Savaria and Claude Thibeault. Probabilistic model checking based DAL analysis to optimize a combined TMR-blind-scrubbing mitigation technique for FPGA-based aerospace applications. In Proc. 12th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'14), pages 175-184, IEEE. 2014. [Uses probabilistic model checking and PRISM to analyse soft-error mitigation techniques and associated dependability properties of SRAM-based FPGAs.]
[LMJ+14] Yu Lu, Alice Miller, Chris Johnson, Zhaoguang Peng and Tingdi Zhao. Availability Analysis of Satellite Positioning Systems for Aviation using the PRISM Model Checker. In Proc. 17th IEEE International Conference on Computational Science and Engineering (CSE'14), IEEE. 2014. [Performs availability analysis of satellite positioning systems for aircraft guidance using probabilistic model checking and PRISM.]
[CS14b] Muffy Calder and Michele Sevegnani. Do I need to fix a failed component now, or can I wait until tomorrow?. In Proc. 10th European Dependable Computing Conference (EDCC'14), pages 70-81, IEEE. 2014. [Proposes methods for operational decision making in complex systems using predictive event-based modelling, probabilistic model checking and PRISM.]
[RC14] José Ignacio Requeno and José Manuel Colom. Analyzing phylogenetic trees with timed and probabilistic model checking: the lactose persistence case study. Journal of Integrative Bioinformatics, 11(3). 2014. [Analyses phylogenetic trees using probabilistic model checking and PRISM.]
[RC14b] José Ignacio Requeno and José Manuel Colom. Timed and Probabilistic Model Checking over Phylogenetic Trees. In 8th International Conference on Practical Applications of Computational Biology & Bioinformatics (PACBB'14), volume 294 of Advances in Intelligent Systems and Computing Volume, pages 105-112, Springer. 2014. [Analyses phylogenetic trees using probabilistic model checking and PRISM.]
[ACHG14] Oana Andrei, Muffy Calder, Matthew Higgs and Mark Girolami. Probabilistic Model Checking of DTMC Models of User Activity Patterns. In Proc. 11th International Conference on Quantitative Evaluation of SysTems (QEST'14), volume 8657 of LNCS, pages 138-153, Springer. 2014. [Analyses user activity patterns modelled as Markov chains using PRISM.]
[MFH+14] Anitha Murugesan, Lu Feng, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael W. Whalen and Insup Lee. Exploring the Twin Peaks using Probabilistic Verification Techniques. In Proc. 4th International Workshop on Twin Peaks of Requirements and Architecture (TwinPeaks'14), ACM. 2014. [Uses probabilistic verification and PRISM as part of an approach to analyse the co-evolution of system requirements and system architecture/design.]
[PLM+14] Zhaoguang Peng, Yu Lu, Alice Miller, Tingdi Zhao and Chris Johnson. Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites. Quality and Reliability Engineering International. 2014. [Uses probabilistic model checking and PRISM to analyse reliability, availability and maintainability properties of a satellite system.]
[GTP14] Debjani Ghosh, Mayank Pandey and Neeraj Tyagi. Stochastic Modelling and Analysis of Video on Demand System with VCR Functionalities. In Proc. 2014 International Computer Science and Engineering Conference (ICSEC'14), pages 78-84, IEEE. 2014. [Uses PRISM to analyse quality-of-service properties of a distributed Video on Demand streaming application.]
[GCB+14] Felipe Pontes Guimaraes, Pedro Célestin, Daniel Macedo Batista, Genaína Nunes Rodrigues and Alba Cristina Magalhaes Alves de Melo. A Framework for Adaptive Fault-Tolerant Execution of Workflows in the Grid: Empirical and Theoretical Analysis. Journal of Grid Computing, 12(1), pages 127-151, Springer. 2014. [Proposes a framework for adaptive fault-tolerant execution of workflows in the grid, including dependability analysis with PRISM. ]
[FBZ14] João M Franco, Raul Barbosa, Mário Zenha-Rela. Availability Evaluation of Software Architectures through Formal Methods. In Proc. 9th International Conference on the Quality of Information. 2014. [Analyses availability constraints on software architectures, including probabilistic model checking with PRISM.]
[DKB14] Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Probabilistic model checking for energy analysis in software product lines. In Proc. 13th international conference on Modularity (MODULARITY'14), pages 169-180, ACM. 2014. [Proposes a compositional modelling framework for software product lines which makes use of PRISM for analysis of system components.]
[DKTT14] Frits Dannenberg, Marta Kwiatkowska, Chris Thachuk and Andrew J. Turberfield. DNA walker circuits: Computational potential, design, and verification. Natural Computing. 2014. [pdf] [bib] [Designs a discrete stochastic model of DNA walker circuits and analyses it with probabilistic model checking and PRISM.]

2013

[PLM+13] Zhaoguang Peng, Yu Lu, Alice Miller, Chris Johnson and Tingdi Zhao. A Probabilistic Model Checking Approach to Analysing Reliability, Availability, and Maintainability of a Single Satellite System. In Proc. 7th European Symposium on Computer Modelling and Simulation (EMS'13), pages 611-616. 2013. [Uses probabilistic model checking and PRISM to analyse reliability, availability and maintainability properties of a satellite system.]
[KV13] Jayanand Asok Kumar and Shobha Vasudevan. Formal Probabilistic Timing Verification in RTL. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(5), pages 788-801, IEEE. 2013. [Analyses timing properties of RTL designs, using the SHARPE tool and a connection to PRISM.]
[JKG13] Benjamin Johnson and Hadas Kress-Gazit. Analyzing and revising high-level robot behaviors under actuator error. In Proc. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'13), pages 741-748. 2013.
[GMZ13] H. Gao, H. Miao and H. Zeng. Predictive web service monitoring using probabilistic model checking. International Journal on Applied Mathematics & Information Sciences, 6(1L), pages 139–148. 2013. [Uses probabilistic model checking and PRISM to predict web service reliability.]
[RSLG13] Mikołaj Rybiński, Zuzanna Szymańska, Sławomir Lasota and Anna Gambin. Modelling the efficacy of hyperthermia treatment. J. R. Soc. Interface, 10(88). 2013. [Analyses models of the effectiveness of hyperthermia in the context of a heat-shock response mechanism, using ODEs and PRISM.]
[BEK+13] Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Selec. In Proc. NASA Formal Methods Symposium (NFM'13), pages 307-321. 2013. [Verifies the Probabilistic-Write/Copy-Select (PWCS) protocol using PRISM.]
[CG13] Sagar Chaki and Joseph Andrew Giampapa. Probabilistic Verification of Coordinated Multi-robot Missions. In Proc. 20th International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 135-153, Springer. 2013. [Proposes techniques to verify multi-robot systems, including the use of PRISM.]
[KATH13] Adil Khurram, Haider Ali, Arham Tariq and Osman Hasan. Formal Reliability Analysis of Protective Relays in Power Distribution Systems. In Proc. International Workshop on Formal Methods for Industrial Critical Systems (FMICS'13), pages 169-183, Springer. 2013. [Models and verifies power distribution relays using PRISM.]
[CK13] Lalit Chandnani and Hemangee K. Kapoor. Formal Approach for DVS-Based Power Management for Multiple Server System in Presence of Server Failure and Repair. IEEE Transactions On Industrial Informatics, 9(1), pages 502-513. 2013. [Uses PRISM to analyse a novel DVS-based power management policy for multiprocessor systems.]
[PBR13] Sophia Petridou, Stylianos Basagiannis and Manos Roumeliotis. Survivability Analysis Using Probabilistic Model Checking: A Study on Wireless Sensor Networks. IEEE Systems Journal, 7(1), pages 4-12. 2013. [Analyses survivability properties of wireless sensor networks using PRISM.]
[YPH13] Guofeng Yan, Yuxing Peng and Bin Huang. State Reachability of Wireless Lossy Channel Systems: Modeling and Probabilistic Analyzing. Journal of Computational Information Systems, 9(4), pages 1381–1388. 2013. [Analyses wireless lossy channel systems using PRISM.]
[Kap13] Tatjana Kapus. Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata. Mobile Information Systems, 9(2), pages 157-188, IOS Press. 2013. [Uses PRISM to build and analyse a probabilistic timed automaton model of the medium access control in nonbeacon-enabled IEEE 802.15.4 wireless personal area networks.]
[TPTL13] Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna and Linas Laibinis. Formal Development and Quantitative Assessment of a Resilient Multi-robotic System. In Proc. 5th International Workshop on Software Engineering for Resilient Systems (SERENE'13), volume 8166 of LNCS, pages 109-124, Springer. 2013. [Analyses the resilience of a multi-robotic system using Event-B and PRISM.]
[KFDK13] Savas Konur, Michael Fisher, Simon Dobson and Stephen Knox. Formal Verification of a Pervasive Messaging System. Formal Aspects of Computing. 2013. [Uses PRISM to apply probabilistic model checking to the analysis of a pervasive message-forwarding system called Scatterboxs]
[Kik13] Shinji Kikuchi. Using Model Checking to Evaluate Live Migrations. IT Professional, 15(2), pages 36-41, IEEE Computer Society. 2013. [Uses probabilistic model checking and PRISM to analyse live migration strategies for cloud computing.]
[DKTT13] Frits Dannenberg, Marta Kwiatkowska, Chris Thachuk and Andrew J. Turberfield. DNA walker circuits: computational potential, design, and verification. In Proc. 19th International Conference on DNA Computing and Molecular Programming (DNA 19), volume 8141 of LNCS, pages 31-45, Springer. September 2013. [pdf] [bib] [Investigates the reliability, performance and correctness of DNA walker circuits using probabilistic model checking and PRISM.]
[CKSW13] Taolue Chen, Marta Kwiatkowska, Aistis Simaitis and Clemens Wiltsche. Synthesis for Multi-Objective Stochastic Games: An Application to Autonomous Urban Driving. In Proc. 10th International Conference on Quantitative Evaluation of SysTems (QEST'13), volume 8054 of LNCS, pages 322-337, Springer. August 2013. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, implemented in PRISM-games, and applies them to an autonomous vehicle case study.]
[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.]
[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.]

2012

[BMJM12] S. Bhatti, S. Memon, I.A. Jokhio and M.A. Memon. Modelling and symmetry reduction of a target-tracking protocol using wireless sensor networks. IET Communications, 6(10), pages 1205-1211. 2012.
[YZN+12] Ender Yüksel, Huibiao Zhu, Hanne Riis Nielson, Heqing Huang and Flemming Nielson. Modelling and Analysis of Smart Grid: A Stochastic Model Checking Case Study. In Proc. 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12), pages 25-32, IEEE. 2012. [Models and verifies a Chinese smart grid implementation using PRISM.]
[BCFCC12] Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos and Sérgio V. A. Campos. A Probabilistic Model Checking Approach to Investigate the Palytoxin Effects on the Na+/K+-ATPase. In Proc. 7th Brazilian Symposium on Bioinformatics (BSB'12). 2012. [Studies the effects of the palytoxin toxin in transmembrane ionic transport systems using various probabilistic model checking tools, including PRISM.]
[LPA+12] Pietro Liò, Nicola Paoletti, Mohammad Ali Moni, Kathryn Atwell, Emanuela Merelli and Marco Viceconti. Modelling osteomyelitis. BMC Bioinformatics, 13(Suppl 14)(S12). 2012. [Describes computational modelling of the bone pathology osteomyelitis, part of which is analysed using PRISM.]
[TPT+12] Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Timo Latvala and Laura Nummila. Formal Development and Assessment of a Reconfigurable On-board Satellite System. In Proc. International Conference on Computer Safety, Reliability, and Security (SAFECOMP'12), pages 210-222. 2012. [Uses Event-B, in conjunction with PRISM, to verify fault tolerance of satellite systems.]
[RASL12] Genaína Nunes Rodrigues, Vander Alves, Renato Silveira and Luiz A. Laranjeira. Dependability Analysis in the Ambient Assisted Living Domain: An Exploratory Case Study. Journal of Systems and Software, 85(1), pages 112-131. 2012. [bib] [Uses PRISM to analyse dependability properties of Ambient Assisted Living systems.]
[KDF12] Savas Konur, Clare Dixon and Michael Fisher. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems, 60(2), pages 199-213. 2012. [bib] [Uses probabilistic model checking and PRISM to analyse the effectiveness of robot swarms.]
[LLL+12] Robyn Lutz, Jack Lutz, James Lathrop, Titus Klinge, Eric Henderson, Divita Mathur and Dalia Abo Sheasha. Engineering and Verifying Requirements for Programmable Self-Assembling Nanomachines. In Proc. 34th ACM/IEEE International Conference on Software Engineering (ICSE'12). 2012. [bib] [Proposes validation techniques for programmable DNA self-assemblies, using DNA origami pliers as an example, and applying PRISM for analysis.]
[CKJ12] Radu Calinescu, Shinji Kikuchi and Kenneth Johnson. Compositional Reverification of Probabilistic Safety Properties for Large-Scale Complex IT Systems. In Proc. 17th Monterey Workshop on Development, Operation and Management of Large-Scale Complex IT Systems. 2012. [Uses PRISM and its compositional (assume-guarantee) extensions to analyse large-scale complex IT systems (LSCITS).]
[LLL+12b] Robyn Lutz, Jack Lutz, James Lathrop, Titus Klinge, Divita Mathur, D. M. Stull, Taylor Bergquist and Eric Henderson. Requirements Analysis for a Product Family of DNA Nanodevices. In Proc. 20th IEEE International Requirements Engineering Conference. 2012. [Applies requirements engineering methods to DNA nanodevices and uses PRISM to verify the generated properties.]
[AASB12] Zaid Al-bayati, O. Ait Mohamed, Yvon Savaria and Mounir Boukadoum. Probabilistic model checking of clock domain crossing interfaces. In Proc. IEEE 10th International New Circuits and Systems Conference (NEWCAS'12). 2012. [Uses PRISM to verify clock domain crossing (CDC) protocols.]
[GHK+12] Lucia Gallina, Tingting Han, Marta Kwiatkowska, Andrea Marin, Sabina Rossi and Alvise Spanò. Automatic Energy-aware Performance Analysis of Mobile Ad-hoc Networks. In Proc. 2012 IFIP Wireless Days conference (WD'12). 2012. [pdf] [Presents a framework for analysing the performance of Mobile Ad-hoc Networks (MANETs) using probabilistic process calculi and PRISM.]
[AB12] Alessandro Aldini and Alessandro Bogliolo. Model Checking of Trust-Based User-Centric Cooperative Networks. In Proc. 4th International Conference on Advances in Future Internet (AFIN'12). 2012.
[LSPM12] Qian Li, Peter Schaffer, Jun Pang and Sjouke Mauw. Comparative Analysis of Clustering Protocols with Probabilistic Model Checking. In Proc. 6th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'12). 2012.
[BPBD12] Manuele Brambilla, Carlo Pinciroli, Mauro Birattari and Marco Dorigo. Property-driven Design for Swarm Robotics. In Proc. 11th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'12). 2012. [Uses probabilistic model checking and PRISM as part of a design process for swarm robotics.]
[HYF+12] Kang He, Hongli Yang, Yachao Feng, Yuan Liu and Zongyan Qiu. Performance Analysis of Data Gathering Protocol Using PRISM. In Proc. 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'12), pages 96-105. 2012. [Uses PRISM to analyse the Power Efficient Algorithm for Data Gathering (PEADG) protocol.]
[OJMD12] Samir Ouchani, Yosr Jarraya, Otmane Ait Mohamed and Mourad Debbabi. Probabilistic Attack Scenarios to Evaluate Policies over Communication Protocols. Journal of Software, 7(7), pages 1488-1495. 2012. [Analyses communication protocol attack scenarios with PRISM, using RTSP/SRTP as an example.]
[LJL+12] Lixing Li, Zhi Jin, Ge Li, Liwei Zheng and Qiang Wei . Modeling and Analyzing the Reliability and Cost of Service Composition in the IoT: A Probabilistic Approach. In Proc. 19th IEEE International Conference on Web Services (ICWS'12), pages 584-591 . 2012. [Uses PRISM to analyse compositions of web services.]
[PB12] Sophia Petridou and Stylianos Basagiannis. Towards Energy Consumption Evaluation of the SSL Handshake Protocol in Mobile Communications. In Proc. 9th IEEE Annual Conference on Wireless on-demand Networks Systems and Services (IEEE WONS'12). 2012. [Analyses the energy consumption of the SSL handshake protocol using a PRISM CTMC model.]
[AC12] Oana Andrei and Muffy Calder. Trend-Based Analysis of a Population Model of the AKAP Scaffold Protein. Transactions on Computational Systems Biology, XIV, pages 1-25, Springer. 2012. [Studies the AKAP scaffold protein by introducing a notion of stochastic trends and using PRISM for model analysis.]
[BBOM12] Paolo Ballarini, Jalel Ben-Othman and Lynda Mokdad. Quantitative Verification of WiMAX Traffic Shaping Solutions. In Proc. 7th International Symposium on Intelligent System Techniques for Ad hoc and Wireless Sensor Networks (IST-AWSN). 2012. [Uses probabilistic model checking and PRISM to analyse traffic-shaping schemes for the IEEE 802.16 (WiMAX) standard.]
[SSK+12] Emmanouela Stachtiari, Yannis Soupionis, Panagiotis Katsaros, Anakreontas Mentis and Dimitris Gritzalis. Probabilistic model checking of CAPTCHA admission control for DoS resistant anti-SPIT protection. In Proc. 7th International Conference on Critical Information Infrastructures Security (CRITIS'12). 2012. [Studies the effectiveness of admission control policies for DoS-resistanct CAPTCHA schemes using probabilistic model checking and PRISM.]
[YTP+12] Qixia Yuan, Panuwat Trairatphisan, Jun Pang, Sjouke Mauw, Monique Wiesinger and Thomas Sauter. Probabilistic Model Checking of the PDGF Signaling Pathway. Transactions on Computational Systems Biology, XIV, pages 151-180. 2012. [Analyses the PDGF signalling pathway using PRISM.]
[LR12] Adalberto Llarena and David Rosenblueth. Model Checking Applied to Humanoid Robotic Soccer. In Advances in Autonomous Robotics, volume 7429 of LNCS, Springer. 2012. [Uses PRISM to synthesise parameters of probabilistic strategies for humanoid robotic football.]
[CCN12] Luca Cardelli and Attila Csikász-Nagy. The Cell Cycle Switch Computes Approximate Majority. Nature Scientific Reports, 2. 2012. [Studies the cell cycle switch as a computing device, based on deterministic/stochastic simulation and probabilistic verification with PRISM.]
[TTL12] Anton Tarasyuk, Elena Troubitsyna and Linas Laibinis. Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In Proc. 9th International Conference on Integrated Formal Methods (IFM'12), pages 237-252. 2012. [Uses PRISM to analyse dynamic service architectures modelled in a probabilistic extension of Event-B.]
[KH12] K. Kobayashi and K. Hiraishi. Symbolic approach to verification and control of deterministic/probabilistic Boolean networks. IET Systems Biology, 6(6), pages 215-222. 2012. [Applies PRISM to the analysis of probabilistic Boolean networks, using an apoptosis network and a WNT5A network as examples.]
[CDKM12b] Taolue Chen, Marco Diciolla, Marta Kwiatkowska and Alexandru Mereacre. Quantitative Verification of Implantable Cardiac Pacemakers. In Proc. 33rd IEEE Real-Time Systems Symposium (RTSS'12), pages 263-272, IEEE. December 2012. [pdf] [Proposes quantitative verification techniques for the analysis of pacemaker software, using the tools PRISM and MATLAB.]
[KNP12a] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Verification of Herman’s Self-Stabilisation Algorithm. Formal Aspects of Computing, 24(4), pages 661-670, Springer. July 2012. [pdf] [bib] [Analyses Herman's self stabilisation protocol using PRISM.]
[LPC+12] Matthew Lakin, David Parker, Luca Cardelli, Marta Kwiatkowska and Andrew Phillips. Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking. Journal of the Royal Society Interface, 9(72), pages 1470-1485, The Royal Society. July 2012. [pdf] [bib] [Analyses correctness, reliability and performance of DNA computing designs using PRISM and DSD.]
[BN12] Péter Biró and Gethin Norman. Analysis of Stochastic Matching Markets. In Proc. 3rd Workshop on Cooperative Games in Multiagent Systems (CoopMAS'12). June 2012. [pdf] [Studies "Stable Matching" problems, including a DTMC-based analysis using PRISM.]

2011

[Bak11] Rena Bakhshi. Gossiping Models: Formal Analysis of Epidemic Protocols. Ph.D. thesis, Vrije Universiteit, Amsterdam. 2011. [bib] http://dare.ubvu.vu.nl/handle/1871/18387
[DYL+11] Chen Deng, Hongli Yang, Husheng Liao, Meng Sun and Zongyan Qiu. Analysis of WS-BPEL Processes in PRISM. In 199-202, pages Proc. 5th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'11). 2011. [Uses PRISM to analyse processes specified in the Web Services Business Process Execution Language (WS-BPEL). ]
[BPA+11] Stylianos Basagiannis, Sophia Petridou, Nikolaos Alexiou, Georgios Papadimitriou and Panagiotis Katsaros. Quantitative analysis of a certified e-mail protocol in mobile environments: A probabilistic model checking approach. Computers & Security, 30(4), pages 257–272, Elsevier. 2011. [bib] [Analyses the Certified E-mail Message Delivery (CEMD) protocol using PRISM.]
[PBA+11] Sophia Petridou, Stylianos Basagiannis, Nikolaos Alexiou, Georgios Papadimitriou and Panagiotis Katsaros. Quantitative Model Checking of an RSA-based Email Protocol on Mobile Devices. In Proc. 16th IEEE Symposium on Computers and Communications (ISCC'11). 2011. [bib] [Analyses the Certified E-mail Message Delivery (CEMD) protocol using PRISM.]
[PBP11] Ioannis Paparrizos, Stylianos Basagiannis and Sophia Petridou. Quantitative Analysis for Authentication of Low-cost RFID Tags. In Proc. 36th IEEE Conference on Local Computer Networks (LCN'11), IEEE. 2011. [Analyses the computation and transmission costs of RFID tags using a PRISM DTMC model.]
[TNBB11] Amir Tavala, Soroosh Nazema and Ali A. Babaei-Brojeny. Verification of Quantum Protocols with a Probabilistic Model-Checker. In Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008), volume 270 of ENTCS, pages 175-182. 2011. [bib]
[DDBM11] M. P. Dobay, A. Dobay, J. Bantang and E. Mendoza. How many trimers? Modeling influenza virus fusion yields a minimum aggregate size of six trimers, three of which are fusogenic. Molecular BioSystems. 2011. [bib]
[CDLPB11] Igor Cizelj, Xu Chu Ding, Morteza Lahijanian, Alessandro Pinto and Calin Belta. Probabilistically Safe Vehicle Control in a Hostile Environment. In Proc. 18th World Congress of the International Federation of Automatic Control (IFAC). 2011. [bib] http://hyness.bu.edu/calin/Publications.html
[YPM+11] Qixia Yuan, Jun Pang, Sjouke Mauw, Panuwat Trairatphisan, Monique Wiesinger and Thomas Sauter. A Study of the PDGF Signaling Pathway with PRISM. In Proc. 3rd International Workshop on Computational Models for Cell Processes (COMPMOD'11), volume 68 of EPTCS, pages 65-81. 2011.
[LMP11] Pietro Liò, Emanuela Merelli and Nicola Paoletti. Multiple verification in computational modeling of bone pathologies. In Proc. 3rd International Workshop on Computational Models for Cell Processes (COMPMOD'11), volume 68 of EPTCS, pages 82-96. 2011. [bib]
[FGHM11] V. Fern'ández, M.-J. Garc'ia-Mart'inez, L. Hern'andez-Encinas and A. Marti'in. Formal Verification of the Security of a Free-Space Quantum Key Distribution System. In Proc. 2011 World Congress in Computer Science, Computer Engineering, and Applied Computing (WORLDCOMP'11), 2011 International Conference on Security and Management (SAM'11). 2011. [bib]
[TK11] Li Tan and Axel Krings. An Adaptive N-variant Software Architecture for Multi-Core Platforms: Models and Performance Analysis. In Proc. International Conference on Computational Science and Its Applications, Part II (ICCSA'11), pages 490-505. 2011. [bib]
[CDGFS11] J. Clement, C. Delporte-Gallet, H. Fauconnie and M. Sighireanu. Guidelines for the Verification of Population Protocols. In Proc. 31st International Conference on Distributed Computing Systems (ICDCS'11). 2011. [bib]
[DKBS11] Tushar Deshpande, Panagiotis Katsaros, Stylianos Basagiannis and Scott Smolka. Formal Analysis of the DNS Bandwidth Amplification Attack and Its Countermeasures Using Probabilistic Model Checking. In Proc. 13th IEEE International Symposium on High-Assurance Systems Engineering (HASE'11), pages 360-367. 2011. [bib]
[MZ11] Ravie C. Muniyandi and Abdullah M. Zin. Membrane Computing as a Modeling Tool for Discrete Systems. Journal of Computer Science, 7(11), pages 1667-1673. 2011. [bib]
[MZ11b] Ravie C. Muniyandi and Abdullah M. Zin. Evaluating Ligand-Receptor Networks of TGF-β with Membrane Computing. Pakistan Journal of Biological Sciences, 14, pages 1100-1108. 2011. [bib]
[MST11a] Tamara Mendt, Carsten Sinz and Olga Tveretina. Probabilistic Model Checking of Constraints in a Supply Chain Business Process. In Business Information Systems, volume 87 of Lecture Notes in Business Information Processing, pages 1-12. 2011.
[NIOK11] T. Nagaoka and A. Ito and K. Okano and S. Kusumoto. QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation. IEICE Transactions on Information and Systems, E94.D(5), pages 958-966 . 2011.
[Dut11] Bruno Dutertre. Probabilistic Analysis of Distributed Fault-Tolerant Systems. Technical report CR–2011-217090, NASA. 2011. http://ntrs.nasa.gov/search.jsp?R=20110011564
[KF11] Savas Konur and Michael Fisher. Formal Analysis of a VANET Congestion Control Protocol through Probabilistic Verification. In Proc. 73rd IEEE Vehicular Technology Conference (VTC'11). 2011.
[Fru11] Matthias Fruth. Formal Methods for the Analysis of Wireless Network Protocols. Ph.D. thesis, Oxford University. October 2011. [pdf] [bib] [Analyses wireless network protocols such as Zigbee using probabilistic model checking and PRISM.]
[KM11] Shinji Kikuchi, Yasuhide Matsumoto. Performance Modeling of Concurrent Live Migration Operations in Cloud Computing Systems using PRISM Probabilistic Model Checker. In Proc. 4th International Conference on Cloud Computing (IEEE Cloud 2011). July 2011. [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.]
[YNN+11] Ender Yüksel‚ Hanne Riis Nielson‚ Flemming Nielson‚ Matthias Fruth and Marta Kwiatkowska. Optimizing Key Updates in Sensor Networks. In Proc. IEEE Sensors Applications Symposium (SAS'11), pages 82-87. February 2011. [bib] [Analyses the performance of ZigBee security key updates using PRISM.]

2010

[ZBB10] Hafedh Zayani, Kamel Barkaoui and Rahma Ben Ayed. Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol. International Journal of Wireless & Mobile Networks, 2(2), pages 156-170. 2010. [bib]
[GPM10] X. Ge, R. Paige and J. McDermid. Analysing System Failure Behaviours With PRISM. In Proc. 4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, pages 130-136. 2010. [bib]
[ABK+10] N. Alexiou, S. Basagiannis, P. Katsaros, T. Dashpande and S. Smolka. Formal Analysis of the Kaminsky DNS Cache-Poisoning Attack Using Probabilistic Model Checking. In Proc. IEEE 12th International Symposium on High-Assurance Systems Engineering (HASE'10), pages 94-103. 2010. [bib] http://www.cs.sunysb.edu/~sas/kaminsky/
[And10] E. André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, L'École Normale Supérieure de Cachan. 2010. [bib] http://www.lsv.ens-cachan.fr/~andre/
[GO10] Matthias Gudemann and Frank Ortmeier. Probabilistic Model-Based Safety Analysis. In Proc. Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010). 2010.
[KV10] J. A. Kumar and S. Vasudevan. Statistical guarantees of performance for MIMO designs. In Proc. IEEE/IFIP International Conference on Dependable Systems & Networks (DSN'10). 2010. [bib]
[KV10b] J. A. Kumar and S. Vasudevan. Automatic compositional reasoning for probabilistic model checking of hardware designs. In Proc. 7th International Conference on Quantitative Evaluation of SysTems (QEST'10), IEEE CS Press. 2010. [bib]
[STK+10] D. Schumm, O. Turetken, N. Kokash, A. Elgammal, F. Leymann and W.-J. van den Heuvel. Business Process Compliance through Reusable Units of Compliant Processes. In Proc. 10th International Conference on Current Trends in Web Engineering (ICWE'10). 2010. [bib]
[KH10] K. Kobayashi and K. Hiraishi. Reachability analysis of probabilistic Boolean networks using model checking. In Proc. SICE Annual Conference 2010, pages 829-832. 2010. [bib]
[RAFL10] G. N. Rodrigues, V. Alves, R. Franklin and L. Laranjeira. Dependability Analysis in the Ambient Assisted Living Domain: an Exploratory Case Study. In Proc. 4th Brazilian Symposium on Software Components, Architectures and Reuse, pages 150-159. 2010. [bib]
[YZH+10] Hongli Yang, Liang Zhou, Kang He, Chen Deng, Xiangpeng Zhao and Zongyan Qiu. A probabilistic QoS model-checking for dynamic routing protocol. In Proc. 10th International Conference on Quality Software (QSIC'10), pages 441-448, IEEE. 2010. [bib]
[OGS10] P. Oliveira, R. Gomes and M. Song. Large Scale Genetic Identity Inference Using Probabilistic Model Checking. In 2010 IEEE International Conference on Systems Man and Cybernetics (SMC'10), pages 3508-3512, IEEE. 2010. [bib]
[KSB10] Heiko Koziolek, Bastian Schlich and Carlos Bilich. A Large-Scale Industrial Case Study on Architecture-based Software Reliability Analysis. In Proc. IEEE 21st International Symposium on Software Reliability Engineering (ISSRE'10), pages 279-288. 2010. [bib]
[HWHY10] Wei Huang, Gengyu Wei, Nan Hu and Yixian Yang. Design and Analysis of Heartbeat Protocol in NIDS Cluster. In Proc. 2nd International Conference on Future Computer and Communication (ICFCC'10). 2010.
[KDF10] Savas Konur, Clare Dixon and Michael Fisher. Formal Verification of Probabilistic Swarm Behaviours. In Proc. 7th International Conference on Swarm Intelligence (ANTS'10), volume 6234 of LNCS, pages 440-447, Springer. 2010. [bib]
[BMA10] Cristiano Bertolini, Alexandre Mota and Eduardo Aranha. Calibrating Probabilistic GUI Testing Models Based on Experiments and Survival Analysis. In Proc. 21st IEEE International Symposium on Software Reliability Engineering (ISSRE'10), pages 319-328. 2010. [Uses PRISM to evaluate software testing techniques for graphical user interfaces.]
[GMS+10] Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe Ferri and Julio Buzzi. Systematic Model-Based Safety Assessment Via Probabilistic Model Checking. In 4th International Symposium on Leveraging Applications on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'10), pages 625-639, Springer. 2010. [Uses PRISM for quantitative safety assessment, with a case study of an actuator control system.]
[YK10] Haidi Yue and Joost-Pieter Katoen. Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption. In Proc. 17th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA'10) , volume 6148 of LNCS, pages 247–261, Springer. 2010. [Analyses a randomised leader election protocol using PRISM.]
[GKMMQ10] Felicita Di Giandomenico, Marta Kwiatkowska, Marco Martinucci, Paolo Masci, and Hongyang Qu. Dependability Analysis and Verification for Connected Systems. In Tiziana Margaria and Bernhard Steffen (editors), 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'10), volume 6416 of LNCS, pages 263-277, Springer. October 2010. [pdf] [Describes a framework for analsyis of connected systems, including probabilistic model checking using PRISM.]

2009

[MKUM09] Paulo Maia, Jeff Kramer, Sebastián Uchitel and Nabor Mendonça. Towards accurate probabilistic models using state refinement. In Proc. 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/SIGSOFT FSE'09), pages 281-284. 2009. [Presents state refinement techniques for generating accurate probabilistic models which are analysed using PRISM.]
[MDT09] Nils Mullner, Abhishek Dhama and Oliver Theel. Deriving a Good Trade-off Between System Availability and Time Redundancy. In Proc. Symposia and Workshops on Ubiquitous, Autonomic and Trusted Computing (UIC-ATC'09), IEEE. 2009. [Studies design trade-offs in self-stabilising systems using several methods, including probabilistic model checking with PRISM.]
[BM09] Cristiano Bertolini and Alexandre Mota. Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. In Proc. 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09). 2009. [bib] http://www.cin.ufpe.br/~cb2/ [Uses PRISM to evaluate software testing techniques for graphical user interfaces.]
[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]
[BMM09] Paolo Ballarini, Radu Mardare and Ivan 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]
[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]
[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]
[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]
[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]
[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] [Proposes a reinforcement framework for collaborative monitoring of security violations and anlayses it using PRISM.]
[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]
[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]
[CV09] M. Casadei and M. Viroli. Using probabilistic model checking and simulation for designing self-organizing systems. In Proc. ACM Symposium on Applied Computing (SAC'2009), pages 2103-2104. 2009. [bib]
[JM09] L. Jagadeesan and V. Mendiratta. Voice Communication Mashups: Formal Specification and Composition of Service Level Agreements. In 3rd International Conference on Next Generation Mobile Applications, Services and Technologies (NGMAST'09). 2009. [bib]
[STTK09] Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Koichi Takahashi and Tohru Kikuno. Probabilistic Model Checking of the One-Dimensional Ising Model. IEICE Transactions on Information and Systems, E92.D(5), pages 1003-1011. 2009. [bib]
[Wer09] Frank Werner. Applied Formal Methods in Wireless Sensor Networks. Ph.D. thesis, University of Karlsruhe. 2009.
[KH09b] M. Kwiatkowska and J. Heath. Biological pathways as communicating computer systems. Journal of Cell Science, 122(16), pages 2793-2800. August 2009. [bib] http://jcs.biologists.org/cgi/content/abstract/122/16/2793 [Describes the application of various computational tools, including PRISM, to systems biology.]
[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]
[KNPV09] Marta Kwiatkowska, Gethin Norman, David Parker and Maria Grazia Vigliotti. Probabilistic Mobile Ambients. Theoretical Computer Science, 410(12-13), pages 1272-1303, Elsevier. March 2009. [ps.gz] [pdf] [bib] [Presents a probabilistic version of the Mobile Ambients calculus and an accompanying case study using PRISM.]

2008

[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] http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=4591503&arnumber=4591526&count=285&index=22
[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] http://prophesy.cs.tamu.edu/publications.html
[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] http://ieeexplore.ieee.org/xpl/tocresult.jsp?isnumber=4459341&isYear=2008
[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] http://www.win.tue.nl/~evink/research/publications.html
[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] http://lsi.epfl.ch/page13139.html
[VD08] Bogdan Vukobratović and Stanisa Dautović. Probabilistic Model Checking of Resistive Electrical Circuits. In Proc. 16th Telecommunications Forum (TELFOR'08), pages 508-511. 2008. [bib]
[GRV08] Uwe Glässer, Sarah Rastkar and Mona Vajihollahi.. Modeling and Validation of Aviation Security. In Intelligence and Security Informatics, pages 337-355. 2008. [bib]
[Dou08] Douglas Graham. Parameterised Verification of Randomised Distributed Systems using State-based Models. Ph.D. thesis, University of Glasgow. 2008. [bib] http://theses.gla.ac.uk/95/01/2008GrahamPhD.pdf
[Tan08] Li Tan. Model check stochastic supply chains. In Proc. IEEE International Conference on Information Reuse and Integration (IRI'08), pages 416 - 421. 2008.
[Ma08] Zhongdan Ma. Modelling with PRISM of Intelligent System. Masters thesis, University of Oxford. 2008. [pdf] [bib] [Uses PRISM to analyse the hand washing problem, in the context of intelligent systems to assist people with dementia.]
[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]
[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]
[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]
[Gar08] L. Gardelli. Engineering Self-Organising Systems with the Multiagent Paradigm. Ph.D. thesis, University of Bologna. 2008. [bib]
[IZ08] S. Islam and M. Zaid. Probabilistic analysis of the ASW protocol using PRISM. In IEEE Southeastcon 2008, pages 159-164. 2008. [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] http://www.ida.liu.se/~rtslab/publications/publications.shtml
[KNP08d] Marta Kwiatkowska, Gethin Norman and David Parker. Analysis of a Gossip Protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36(3), pages 17-22. December 2008. [pdf] [bib] [Analyses a gossip protocol for information dissemination using PRISM.]
[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] http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=4435957&arnumber=4378215
[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] [Thesis developing computational models of the FGF and Wnt pathways, including the use of PRISM.]
[HKN+08] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker and Oksana 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] [Analyses the FGF (Fibroblast Growth Factor) signalling pathway using PRISM.]

2007

[HVH07] Tran Thi Bich Hanh and Dang Van Hung. Verification of an Air-Traffic Control System with Probabilistic Real-time Model-checking. Technical report , UNU-IIST United Nations University International Institute for Software Technology. 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]
[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] http://www.springerlink.com/content/h0438p764643727u/
[Kal07] E. Kaldeli. Investigating formal representations of PIN block attacks. Masters thesis, School of Informatics, University of Edinburgh. 2007. [bib] http://www.inf.ed.ac.uk/publications/thesis/online/IM070467.pdf
[KNP07b] Marta Kwiatkowska, Gethin Norman and David Parker. Controller Dependability Analysis By Probabilistic Model Checking. Control Engineering Practice, 15(11), pages 1427-1434, Elsevier. November 2007. [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.]
[STKT07] Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno and Koichi Takahashi. Analyzing the One Dimensional Ising Model by Probabilistic Model Checking. In Proc. IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007). October 2007.
[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]
[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]
[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] http://www.itee.uq.edu.au/~kirsten/
[Vys07] V. Vyshemirsky. Probabilistic Reasoning and Inference for Systems Biology. Ph.D. thesis, University of Glasgow. July 2007. [bib] http://www.dcs.gla.ac.uk/~vvv/
[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] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[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] http://www.liacs.nl/~devink/research/publications.html
[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] http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4063343
[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] http://si2.epfl.ch/~susu/pubs.html

2006

[Ste06] G. Steel. Formal Analysis of PIN Block Attacks. Theoretical Computer Science, 367(1-2), pages 257-270, Elsevier. 2006. [bib]
[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] http://www.dcs.gla.ac.uk/~muffy/papers.html
[Tro06] A. Troina. Probabilistic Timed Automata for Security Analysis and Design. Ph.D. thesis, University of Pisa. 2006. http://www.lix.polytechnique.fr/~troina/
[Adi06] M. Adithia. Probabilistic Analysis of Network Anonymity using PRISM. Masters thesis, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven. 2006. [bib] http://alexandria.tue.nl/extra1/afstversl/wsk-i/adithia2006.pdf
[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] http://www.jucs.org/jucs_12_8/variations_on_itai_rodeh
[Che06] L. Cheung. Reconciling Nondeterministic and Probabilistic Choices. Ph.D. thesis, Radboud University of Nijmegen. 2006. [bib] http://theory.csail.mit.edu/~lcheung/
[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] http://www.cse.unsw.edu.au/~ansgar/
[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] http://www.cs.kent.ac.uk/people/staff/dfc/site/
[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. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html
[BFW06b] Paolo Ballarini, Michael Fisher and Michael Wooldridge. Uncertain Agent Verification through Probabilistic Model-Checking. In Proc. 3rd International Workshop on Safety and Security in Multi-agent Systems (SASEMAS'06). 2006. [bib]
[MF06] Annabelle McIver and Ansgar Fehnker. Formal Techniques for the Analysis of Wireless Networks. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'06), pages 263–270. 2006. [Applies various formal verification techniques to wireless networks, including probabilistic model checking with PRISM.]
[BM06] Paolo Ballarini and Alice Miller. Model Checking Medium Access Control for Sensor Networks. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods (ISoLA'06), pages 255-262. 2006. [Uses PRISM to verify S-MAC, a medium access control protocol for wireless sensor networks.]
[DKNP06] Marie Duflot, Marta Kwiatkowska, Gethin Norman and David 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] [Analyses device discovery in Bluetooth using PRISM.]
[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]
[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] [Analyses several fair exchange and contract signing protocols using PRISM.]
[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.]
[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] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[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] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[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] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[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] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[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] http://www.iist.unu.edu/~dvh/publications_2.html
[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. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html
[BFW06] Paolo Ballarini, Michael Fisher and Michael 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] http://www.csc.liv.ac.uk/~mjw/pubs/

2005

[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] http://linkinghub.elsevier.com/retrieve/pii/S1571066105001854
[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] http://theory.csail.mit.edu/~lcheung/
[NPKS05] Gethin Norman, David Parker, Marta Kwiatkowska and Sandeep 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] [Analyses the reliability of defect-tolerant design, NAND multiplexing, using PRISM.]
[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] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[Bal05] Paolo 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] http://www.csc.liv.ac.uk/~paolo/
[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.]
[BP05] M. Bhargava and C. Palamidessi. Probabilistic Anonymity. In Proc. 16th International Conference on Concurrency Theory (CONCUR'05). August 2005. [bib] http://www.lix.polytechnique.fr/~catuscia/papers/Anonymity/report.pdf
[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] http://www.lix.polytechnique.fr/~catuscia/papers/Anonymity/report_wa.pdf
[NPK+05] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev 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] [Analyses probabilistic dynamic power management (DPM) strategies using PRISM.]
[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]
[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] http://fmt.isti.cnr.it/~mtbeek/
[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]
[KNP05d] Marta Kwiatkowska, Gethin Norman and David 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] [Gives an overview of PRISM and describes a selection of case studies.]
[GNP05] S. Gay, R. Nagarajan and N. Papanikolaou. Probabilistic Model Checking of Quantum Protocols. Quantum Physics Repository article quant-ph/0504007. April 2005. http://arxiv.org/abs/quant-ph/0504007
[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] http://www.cse.unsw.edu.au/~carrollm/probs/Papers/McIver-05c.pdf
[KNP05b] Marta Kwiatkowska, Gethin Norman and David 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] [Surveys a selection of case studies that have been carried out using PRISM.]
[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] http://www.dcs.warwick.ac.uk/~nikos/
[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] http://www.dcs.gla.ac.uk/~muffy/papers.html
[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] http://fmt.isti.cnr.it/WEBPAPER/TRdsvis.pdf
[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] http://www.cse.ucsd.edu/~gupta/pubs/TVLSIEnergy05.pdf

2004

[Shm04] V. Shmatikov. Probabilistic Model Checking of an Anonymity System. Journal of Computer Security, 12(3/4), pages 355-377. 2004. [bib] http://www.cs.utexas.edu/~shmat/index.html
[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.]
[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]
[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] http://www.lix.polytechnique.fr/~pangjun/research/pub.html
[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] http://www.csl.sri.com/users/shmat/
[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. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html#Recent Publications
[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.]
[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] http://www.di.unipi.it/~troina/
[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]
[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.]
[Pap04] N. Papanikolaou. Techniques for Design and Validation of Quantum Protocols. Masters thesis, Department of Computer Science, University of Warwick. 2004. http://www.warwick.ac.uk/~essiai/publications/index.html

2003

[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.]
[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] 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.]
[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]
[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]
[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] http://www.cs.utexas.edu/~shmat/index.html

2001

[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] [Analyses Aspnes and Herlihy's randomised consensus protocol using PRISM and Cadence SMV.]

Underlying techniques in PRISM

2020

[KNPS20b] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Multi-player Equilibria Verification for Concurrent Stochastic Games. In Proc. 17th International Conference on Quantitative Evaluation of SysTems (QEST'20), Springer. August 2020. [pdf] [bib] [Presents techniques for model checking CSGs against equilibria-based properties over multiple coalitions, implemented in PRISM-games.]

2019

[KNP19] Marta Kwiatkowska, Gethin Norman and David Parker. Verification and Control of Turn-Based Probabilistic Real-Time Games. In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday), volume 11760 of LNCS, pages 379-396, Springer. November 2019. [pdf] [bib] [Proposes techniques for verifying probabilistic real-time games building on methods implemented in PRISM-games.]
[KNPS19] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 298-315, Springer. October 2019. [pdf] [bib] [Develops verification methods for stochastic games using Nash equilibria, implemented in PRISM-games.]

2018

[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), volume 11024 of LNCS, pages 223-239, Springer. September 2018. [pdf] [bib] [Proposes verification techniques for concurrent stochastic games, and implements and evaluates them in an extension of PRISM-games.]

2017

[BKW17] Nicolas Basset, Marta Kwiatkowska and Clemens Wiltsche. Compositional Strategy Synthesis for Stochastic Games with Multiple Objectives. Information and Computation. To appear. 2017. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, along with a compositional assume-guarantee strategy synthesis framework.]
[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 verification 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.]

2016

[Dan16] Frits Dannenberg. Modelling and verification for DNA nanotechnology. Ph.D. thesis, Department of Computer Science, University of Oxford. 2016. [pdf] [bib] [Develops models of DNA nanotechnology designs, based on continuous-time Markov chains, and associated model checking techniques.]
[vEJPV16] Christian von Essen, Barbara Jobstmann, David Parker and Rahul Varshneya. Synthesizing Efficient Systems in Probabilistic Environments. Acta Informatica, 53(4), pages 425–457, Springer. June 2016. [pdf] [bib] [Proposes efficient techniques for synthesising strategies in Markov decision processes against ratio objectives, implemented in an extension of PRISM.]
[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.]

2015

[DFK+15] Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems. Logical Methods in Computer Science, 11(2). 2015. [pdf] [bib] [Proposes techniques for permissive controller synthesis on stochastic games, implemented in an extension of PRISM.]
[Ujm15] Mateusz Ujma. On Verification and Controller Synthesis for Probabilistic Systems at Runtime. Ph.D. thesis, Department of Computer Science, University of Oxford. 2015. [pdf] [bib] [Develops various techniques for probabilistic verification and controller synthesis at runtime: incremental model checking, permissive controller synthesis and learning-based controller synthesis.]
[Wil15] Clemens Wiltsche. Assume-Guarantee Strategy Synthesis for Stochastic Games. Ph.D. thesis, Department of Computer Science, University of Oxford. 2015. [pdf] [bib] [Develops strategy synthesis techniques for stochastic games, in particular, compositional methods based on assume-guarantee rules.]
[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.]
[BKTW15] Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of LNCS, pages 256-271, Springer. April 2015. [pdf] [bib] [Proposes strategy synthesis for stochastic games with multiple long-run objectives, implemented in an extension of PRISM.]

2014

[CDKP14] Milan Ceska, Frits Dannenberg, Marta Kwiatkowska and Nicola Paoletti. Precise Parameter Synthesis for Stochastic Biochemical Systems. In Proc. 12th International Conference on Computational Methods in Systems Biology (CMSB'14), volume 8859 of LNCS/LNBI, pages 86-98, Springer. November 2014. [pdf] [bib] [Proposes parameter synthesis techniques for CSL properties on stochastic biochemical networks, to implemented in PRISM.]
[BKW14] Nicolas Basset, Marta Kwiatkowska and Clemens Wiltsche. Compositional Controller Synthesis for Stochastic Games. In P. Baldan and D. Gorla (editors), Proc. 25th International Conference on Concurrency Theory (CONCUR'14), volume 8704 of LNCS, pages 173-187, Springer. September 2014. [pdf] [bib] [Proposes compositional assume-guarantee strategy synthesis techniques for stochastic 2-player games.]
[Sim14] Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. Ph.D. thesis, Department of Computer Science, University of Oxford. March 2014. [pdf] [bib] [Presents novel techniques for verification using stochastic multi-player games and implements them in PRISM-games, an extension of PRISM.]

2013

[KNPQ13] Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu. Compositional Probabilistic Verification through Multi-Objective Model Checking. Information and Computation, 232, pages 38-65, Elsevier. November 2013. [pdf] [bib] [Presents assume-guarantee verification techniques for probabilistic automata, implemented as an extension of PRISM.]
[DHK13] Frits Dannenberg, Ernst Moritz Hahn and Marta Kwiatkowska. Computing Cumulative Rewards using Fast Adaptive Uniformisation. In Proc. 11th International Conference on Computational Methods in Systems Biology (CMSB'13), volume 8130 of LNCS, pages 33-49, Springer. September 2013. [pdf] [bib] [Develops fast adaptive uniformisation techniques for cumulative reward properties, implemented in PRISM.]
[CFK+13b] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. Formal Methods in System Design, 43(1), pages 61-92, Springer. August 2013. [pdf] [bib] [Introduces model checking techniques for stochastic multi-player games, implemented in the PRISM-games tool.]
[CFK+13c] Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, Aistis Simaitis and Clemens Wiltsche. On Stochastic Games with Multiple Objectives. In Proc. 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), volume 8087 of LNCS, pages 266-277, Springer. August 2013. [pdf] [bib] [Studies strategy synthesis and Pareto set approximation for multiple reward objectives in stochastic 2-player games.]
[CKSW13] Taolue Chen, Marta Kwiatkowska, Aistis Simaitis and Clemens Wiltsche. Synthesis for Multi-Objective Stochastic Games: An Application to Autonomous Urban Driving. In Proc. 10th International Conference on Quantitative Evaluation of SysTems (QEST'13), volume 8054 of LNCS, pages 322-337, Springer. August 2013. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, implemented in PRISM-games, and applies them to an autonomous vehicle case study.]

2012

[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.]
[CFK+12b] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi and Michael Ummels. Playing Stochastic Games Precisely. In 23rd International Conference on Concurrency Theory (CONCUR'12), volume 7454 of LNCS, pages 348-363, Springer. September 2012. [pdf] [bib] [Proposes model checking techniques for stochastic games against temporal logic properties with precise bounds, as implemented in PRISM-games.]
[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.]

2010

[Nim10] Vincent Nimal. Statistical Approaches for Probabilistic Model Checking. MSc Mini-project Dissertation, Oxford University Computing Laboratory. September 2010. [pdf] [bib] [Investigates approximate/statistical model checking techniques and implements them in PRISM.]
[KKNP10] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David 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] [Presents game-based abstraction-refinement techniques for MDPs, as used for example to verify PTAs in 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.]

2009

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

2008

[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] http://www.lmcs-online.org/ojs/viewarticle.php?id=364&layout=abstract

2007

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

2006

[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]
[Wan06] F. Wang. Symbolic Implementation of Model-Checking Probabilistic Timed Automata. Ph.D. thesis, University of Birmingham. September 2006. [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]
[KNPS06] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy 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åkan Younes, Marta Kwiatkowska, Gethin Norman and David 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]

2005

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

2004

[KNP04b] Marta Kwiatkowska, Gethin Norman and David 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] 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.]
[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]

2003

[MPK03b] Rashid Mehmood, David Parker and Marta 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]
[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]
[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]
[HKN+03] Holger Hermanns, Marta Kwiatkowska, Gethin Norman, David Parker and Markus 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]

2002

[Par02] David Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham. 2002. [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]
[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]

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] [ps.gz] [bib]
[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]
[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]

2000

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

Extensions and adaptions to PRISM

2020

[PTHH20] Kittiphon Phalakarn, Toru Takisaka, Thomas Haas and Ichiro Hasuo. Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 349-371, Springer. 2020. [bib] [Develops a bounded value iteration technique for accurate solution of stochastic games, implemented as an extension of PRISM-games.]
[RWWDV20] Nima Roohi, Yu Wang, Matthew West, Geir E. Dullerud and Mahesh Viswanathan. STMC: Statistical Model Checker with Stratified and Antithetic Sampling. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 448-460, Springer. 2020. [bib] [Proposes a technique and tool for statistical model checking using antithetic and stratified sampling, built as an extension of PRISM.]

2019

[Mu19] Chunyan Mu. Automated Game-Theoretic Verification of Security Systems. In Proc. 16th International Conference on Quantitative Evaluation of SysTems (QEST'19), volume 11785 of LNCS, pages 239-256, Springer. 2019. [pdf] [bib] [Develops a game-theoretic approach to verifying security systems building upon PRISM.]
[LP19] Alessio Lomuscio and Edoardo Pirovano. A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems. In Proc. 18th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS'19), pages 161-169. 2019. [Presents techniques for verification of probabilistic swarm systems developed as an extension of PRISM.]
[LFPH19] Bruno Lacerda, Fatma Faruq, David Parker and Nick Hawes. Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots. International Journal of Robotics Research, 38(9), pages 1098–1123. 2019. [pdf] [bib] [Presents a framework for mobile service robot with formal performance guarantees, with an implementation built on PRISM.]
[NKI19] Ali A. Noroozi, Jaber Karimpour and Ayaz Isazadeh. Information leakage of multi-threaded programs. Computers & Electrical Engineering, 78, pages 400-419. 2019. [Presents an approach for quantitative information flow, implemented in PRISM-Leak, an extension of PRISM.]
[EP19] Alexandros Evangelidis and David Parker. Quantitative Verification of Numerical Stability for Kalman Filters. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 425-441, Springer. October 2019. [pdf] [bib] [Builds a framework for verifying Kalman filters on top of PRISM.]
[NP19] Chris Novakovic and David Parker. Automated Formal Analysis of Side-Channel Attacks on Probabilistic Systems. In Proc. 24th European Symposium on Research in Computer Security (ESORICS'19), volume 11735 of LNCS, pages 319-337, Springer. September 2019. [pdf] [bib] [Develops techniques to identify side-channel attacks in probabilistic systems, building on PRISM-pomdps.]

2018

[BCD+18] Christel Baier, Philipp Chrszon, Clemens Dubslaff, Joachim Klein and Sascha Klüppelholz. Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination. In It's All About Coordination. Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab, volume 10865 of LNCS, pages 38-56, Springer. 2018. [Presents an extension of PRISM with multi-action models to analyse exogenous coordination.]
[LP18] Alessio Lomuscio and Edoardo Pirovano. Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems. In Proc. 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI'18), AAAI Press. 2018. https://www.ijcai.org/proceedings/2018/0056.pdf [Proposes verification techniques for probabilistic swarm systems, including an implementation that uses PRISM.]
[KBC+18] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer, 20(2), pages 179-194. 2018. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements.]
[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. October 2018. [pdf] [bib] [Proposes techniques for verified multi-robot task allocation and planning, implemented as an extension of PRISM.]
[Kam18] Nishanthan Kamaleson. Model Reduction Techniques for Probabilistic Verification of Markov Chains. Ph.D. thesis, University of Birmingham. April 2018. [pdf] [bib] [Develops several model reduction techniques, for finite-horizon bisimulation and linear inductive models, and implements them in extensions of PRISM.]
[MDPR18] Chunyan Mu, Peter Dittrich, David Parker and Jonathan E. Rowe. Organisation-Oriented Coarse Graining and Refinement of Stochastic Reaction Networks. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 15(4), pages 1152-1166. February 2018. [pdf] [bib] [Presents techniques for analysing chemical reaction networks, based on chemical organisation theory, and implemented as an extension of PRISM.]

2017

[BKKW17] Christel Baier, Joachim Klein, Sascha Kluppelholz and Sascha Wunderlich. Maximizing the Conditional Expected Reward for Reaching the Goal. In In Proc. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Springer. 2017. [Introduces novel techniques for computing conditional expected rewards in MDPs, implemented in an extension of PRISM.]
[KBC+17] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer. 2017. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements.]
[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.]
[NPZ17] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems, 53(3), pages 354-402, Springer. April 2017. [pdf] [bib] [Presents techniques and a tool for verification and strategy synthesis in partially observable probabilistic models with both discrete and dense models of time.]

2016

[BBBK16] Benoit Barbot, Nicolas Basset, Marc Beunardeau and Marta Kwiatkowska. Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement. In Proc. 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), volume 9826 of LNCS, pages 175-190, Springer. 2016. [pdf] [bib] [Develops Monte Carlo model checking techniques for timed automata using PRISM, SageMath and COSMOS.]
[KBC+16] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz and Steffen Märcker, David Müller. Advances in Symbolic Probabilistic Model Checking with PRISM. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), pages 349-366, Springer. 2016. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements. ]
[KKR16] Lubos Korenciak, Antonin Kucera and Vojtech Rehak. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. In Proc. 24th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'16). 2016. [Proposes fixed-delay synthesis techniques on a variant of continuous-time Markov chains, implemented as an extension of PRISM.]
[CPPBK16] Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim and Marta Kwiatkowska. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), Springer. To appear. April 2016. [pdf] [bib] [Introduces an extension of PRISM in the form of GPU-accelerated tool for parameter synthesis of stochastic systems. ]

2015

[BDE+15] Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. Locks: Picking key methods for a scalable quantitative analysis. Journal of Computer and System Sciences, 81(1), pages 258-287. 2015. [Extends PRISM with support for conditional steady-state queries and then analyses models of low-level operating-system code, using a test-and-test-and-set (TTS) lock as an example.]
[BCFK15] Tomáš Brázdil, Krishnendu Chatterjee, Vojtěch Forejt and Antonín Kučera. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of LNCS, pages 181-187, Springer. 2015. [Presents a tool for multi-objective model checking of mean-payoff properties MDPs, building on several PRISM components.]
[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.]

2014

[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.]
[DKPQ14] Klaus Draeger, Marta Kwiatkowska, David Parker and Hongyang Qu. Local Abstraction Refinement for Probabilistic Timed Programs. Theoretical Computer Science, 538, pages 37-53, Elsevier. June 2014. [pdf] [bib] [Presents new techniques for abstraction refinement on probabilistic timed programs (probabilistic timed automata with data variables), implemented in an extension of PRISM.]
[Gir14] Sergio Giro. Optimal Schedulers vs Optimal Bases: An approach for efficient exact solving of Markov decision processes. Theoretical Computer Science, 538, pages 70–83, Elsevier. June 2014. [pdf] [bib] [Investigates exact-arithmetic model checking methods for MDPs, implemented in an extension of PRISM.]
[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.]

2013

[Tsa13] Tony Tsang. Performance Analysis for QoS-Aware Two- Layer Scheduling in LTE Networks. International Journal of Emerging Trends & Technology in Computer Science (IJETTCS), 2(2). 2013. [Uses an extension of PRISM's simulator to solve scheduling and resource allocation problems.]
[Fen13] Lu Feng. On Learning Assumptions for Compositional Verification of Probabilistic Systems. Ph.D. thesis, University of Oxford. October 2013. [pdf] [bib] [Develops several assume-guarantee techniques for compositional probabilistic verification using automatic generation of assumptions. Implements the techniques using various extensions of PRISM.]
[CHH+13] Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu and Lijun Zhang. Model Repair for Markov Decision Processes. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE'13), pages 85--92, IEEE. July 2013. [pdf] [bib] [Proposes approximate solution methods for the problem of model repair on Markov decision processes, implemented as an extension of PRISM.]

2012

[BDE+12] Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. Waiting for Locks: How Long Does It Usually Take?. In Proc. 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'12). 2012. [Extends PRISM with support for conditional steady-state queries and then analyses models of low-level operating-system code, using a test-and-test-and-set (TTS) lock as an example.]
[WB12] Anton Wijs and Dragan Bosnacki. Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking. In A. Donaldson and D. Parker (editors), Proc. 19th International SPIN Workshop on Model Checking of Software (SPIN'12), volume 7385 of LNCS, pages 98-116, Springer. 2012.
[HMZ+12] David Henriques, Joao G. Martins, Paolo Zuliani, André Platzer and Edmund M. Clarke. Statistical Model Checking for Markov Decision Processes. In Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST'12). 2012. [Develops techniques for statistical model checking of MDPs, built with an extension to PRISM's simulation engine.]
[vEJ12] Christian von Essen and Barbara Jobstmann. Synthesizing Efficient Controllers. In Proc. 13th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'12), volume 7148 of LNCS, pages 428-444, Springer. 2012. [bib] [Presents MDP-based controller synthesis techniques for ratio objectives and implements them in an extension of PRISM.]
[GR12] Sergio Giro and Markus Rabe. Verification of Partial-Information Probabilistic Systems using Counterexample-Guided Refinements. In Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 333-348, Springer. October 2012. [pdf] [bib] [Describes new techniques for model checking MDPs under partial-information schedulers, implemented in an extension of PRISM.]
[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.]
[Gir12] Sergio Giro. Efficient Computation of Exact Solutions for Quantitative Model Checking. In Proc. 10th Workshop on Quantitative Aspects of Programming Languages (QAPL'12), volume 85 of EPTCS, pages 17-32. March 2012. [pdf] [bib] [Investigates exact-arithmetic model checking methods for MDPs, implemented in an extension of PRISM.]

2011

[KG11] Christian Krause and Holger Giese. Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements. In Proc. 13th International Workshop on Verification of Infinite-State Systems (INFINITY'11). 2011. [bib]
[JGB11] Paul Jennings, Arka Ghosh and Samik Basu. A Two-phase Approximation for Model Checking Unbounded Until Properties of Probabilistic Systems. ACM Transactions on Software Engineering and Methodology. 2011. [bib]
[HKQ11] Henri Hansen, Marta Kwiatkowska and Hongyang Qu. Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness. In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST'11), pages 203-212, IEEE CS Press. September 2011. [pdf] [bib] [Presents partial-order reduction methods for MDPs, implemented in an extension of PRISM.]
[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.]
[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.]
[Kat11] Mark Kattenbelt. Automated Quantitative Software Verification. Ph.D. thesis, Oxford University. March 2011. [pdf] [bib] [Thesis on quantitative verification for software, including probabilistic abstraction-refinement methods that use components from GOTO-CC, SATABS and PRISM.]

2010

[AL10] H. Aljazzar and S. Leue. Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking. IEEE Transactions on Software Engineering, 36(1), pages 37-60, IEEE Computer Society. 2010. [bib]
[HGB+10] Ru He, Paul Jennings, Samik Basu, Arka Ghosh and Huaiqing Wu. A bounded statistical approach for model checking of unbounded until properties. In 25th IEEE/ACM International Conference on Automated Software Engineering (ASE'10), pages 225-234. 2010. [bib]
[LWAB10] M. Lahijanian, J. Wasniewski, S. B. Andersson and C. Belta. Motion Planning and Control from Temporal Logic Specifications with Probabilistic Satisfaction Guarantees. In Proc. 2010 IEEE International Conference on Robotics and Automation, pages 3227-3232. 2010. [bib] http://hyness.bu.edu/calin/Publications.html
[BESW10] Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski and Anton Wijs. GPU-PRISM: An Extension of PRISM for General Purpose Graphics Processing Units. In Proc. 9th International Workshop on Parallel and Distributed Methods in Verification. 2010. [bib]
[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.]
[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.]

2009

[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]
[HHWZ09] H. Hermanns, E. M. Hahn, B. Wachter and L. Zhang. Time-bounded model checking of infinite-state continuous-time Markov chains. Fundamenta Informaticae, 95(1), pages 129-155. 2009. [bib]
[BGH09] A. Basu, A. Ghosh and R. He. Approximate Probabilistic Model Checking Using Bounded Until Properties. In Proc. 11th International Conference on Formal Engineering Methods (ICFEM'09),. 2009. [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] [Develops MTBDD variable ordering heuristics, implemented in an extension of PRISM.]
[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] http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=5261015
[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] [Describes verification techniques for probabilistic C programs, using components from GOTO-CC, SATABS and PRISM.]
[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] [Provides an overview of the CONNECT project, which incorporates extensions of PRISM.]
[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.]

2008

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

2007

[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] http://www.sce.carleton.ca/~derisavi/publications/index.html

2005

[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]
[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]
[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] http://sweden.autonomy.ri.cmu.edu/papers/

2004

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

Tool/language connections to PRISM

2020

[RMT+20] Michael Raitza, Steffen Märcker, Jens Trommer, André Heinzig, Sascha Klüppelholz, Christel Baier and Akash Kumar. Quantitative Characterization of Reconfigurable Transistor Logic Gates. IEEE Access. 2020. [Presents formal analysis techniques for logic gates using probabilistic model checking and a toolchain based on PRISM.]
[BP20b] Edoardo Bacci and David Parker. Probabilistic Guarantees for Safe Deep Reinforcement Learning. In Proc. 18th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'20), Springer. To appear. September 2020. [pdf] [bib] [Proposes techniques for probabilistic verification of deep reinforcement learning policies, using PRISM as an underlying model checker.]

2019

[NMMZZ19] Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng and Zhen Zhang. STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis. In Proc. 31st International Conference on Computer Aided Verification (CAV'19), volume 11561 of LNCS, pages 540-549, Springer. 2019. [Describes a tool for probabilistic verification of infinite-state systems, connecting to PRISM's model checking engines.]
[TAB+19] Martin Tappler, Bernhard K. Aichernig, Giovanni Bacci, Maria Eichlseder and Kim G. Larsen. L*-Based Learning of Markov Decision Processes. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 651-669, Springer. 2019. [Performs probabilistic model checking with PRISM as part of an MDP learning framework.]
[EK19] Julia Eisentraut and Jan Kretinsky. Expected Cost Analysis of Attack-Defense Trees. In Proc. 16th International Conference on Quantitative Evaluation of Systems (QEST'19), volume 11785 of LNCS, pages 203-221, Springer. 2019. [bib] [Presents an approach to analysing attack-defence trees using PRISM-games for model checking stochastic games.]
[KDL19] Gildas Kouko, Josée Desharnais and François Laviolette. Finite Approximation of LMPs for Exact Verification of Reachability Properties. In Proc. 16th International Conference on Quantitative Evaluation of Systems (QEST'19), volume 11785 of LNCS, pages 70-87, Springer. 2019. [Proposes techniques for approximate verification of labelled Markov processes using PRISM as an underlying solver.]
[AGK+19] J. Aldrich, D. Garlan, C. Kaestner, C. Le Goues, A. Mohseni-Kabir, I. Ruchkin, S. Samuel, B. Schmerl, C. S. Timperley, M. Veloso, I. Voysey, J. Biswas, A. Guha, J. Holtz, J. Camara and P. Jamshidi. Model-Based Adaptation for Robotics Software. IEEE Software, 36(2), pages 83-90, IEEE. 2019. [Summarises the Model-based Adaptation for Robotics Software (MARS) project; PRISM is used as one of the underlying solvers to verify task plans and architecture reconfigurations.]

2018

[LSM+18b] Morteza Lahijanian, María Svorenová, Akshay A. Morye, Brian Yeomans, Dushyant Rao, Ingmar Posner, Paul Newman, Hadas Kress-Gazit and Marta Kwiatkowska. Resource-Performance Trade-off Analysis for Mobile Robots. IEEE Robotics and Automation Letters, 3(3), pages 1840-1847. 2018. [Proposes a framework for analysing resource-performance trade-offs in mobile robotics, using PRISM as an underlying model checker.]
[LJ18] Nian-Ze Lee and Jie-Hong R. Jiang. Towards Formal Evaluation and Verification of Probabilistic Design. IEEE Transactions on Computers, 67(8), pages 1202-1216, IEEE. 2018. [Uses PRISM as part of a framework to verify approximate and probabilistic designs for circuits.]
[CDKB+18] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. ProFeat: Feature-oriented Engineering for Family-based Probabilistic Model Checking. Formal Aspects of Computing, volume, 30(1), pages 45-75. 2018. [Presents the ProFeat tool for feature-oriented modelling and feature-aware analysis, incorporating PRISM.]

2017

[AVA+17] Arthur Americo, Artur Vaz, Mario S. Alvim, Sergio V. A. Campos and Annabelle McIver. Formal Analysis of the Information Leakage of the DC-Nets and Crowds Anonymity Protocols. In Proc. Brazilian Symposium on Formal Methods, pages 142-158, Springer. 2017. [Studies information leakage in anonymity protocols, building on probabilistic model checking with PRISM.]
[SBJJB17] Jiyoung Song, Young-Min Baek, Mingyu Jin, Eunkyoung Jee and Doo-Hwan Bae. SoS GaP Slicer: Slicing SoS Goal and PRISM Models for Change-Responsive Verification of SoS. In Proc. 2017 24th Asia-Pacific Software Engineering Conference (APSEC'17). 2017. [Presents a slicing technique, based on PRISM models, for statistical model checking of system-of-system models.]
[WJW+17] Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen and Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. In Proc. 56th Annual Conference on Decision and Control (CDC'17), pages 2201-2208, IEEE. 2017. [Develops a game-based abstraction approach to solving POMDPs, including PRISM-games as part of the tool-chain.]
[MSHA17] Mujahid Mohsin, Muhammad Usama Sardar, Osman Hasan and Zahid Anwar. IoTRiskAnalyzer: A Probabilistic Model Checking Based Framework for Formal Risk Analytics of the Internet of Things. IEEE Access, IEEE. 2017. [Presents a framework for formally quantifying risk in Internet of Things applications, using PRISM as the underlying probabilistic model checker.]

2016

[CDKB16] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat. In Proc. 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), volume 9633 of LNCS, pages 287-304, Springer. 2016. [Proposes a formalism for modelling families of probabilistic systems with differing features and a tool for their analysis, which connects to PRISM through model translations.]
[MRAAB16] Danilo Filgueira Mendonça, Genaína Nunes Rodriguesa, Raian Alib, Vander Alvesa and Luciano Baresi. GODA: A goal-oriented requirements engineering framework for runtime dependability analysis. Information and Software Technology, 80, pages 245–264, Elsevier. 2016. [Proposes GODA, a goal-oriented requirements engineering framework for runtime dependability analysis, which uses probabilistic model checking and PRISM for underlying analysis. ]
[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.]

2015

[GTC15] Simos Gerasimou, Giordano Tamburrelli and Radu Calinescu. Search-Based Synthesis of Probabilistic Models for Quality-of-Service Software Engineering. In Proc. 30th IEEE/ACM International Conference on Automated Software Engineering (ASE'15). 2015. [Proposes search-based software engineering techniques using multi-objective optimisation, implemented in the EvoChecker tool which performs model analysis using PRISM.]
[KG15] Savas Konur and Marian Gheorghe. A Property-Driven Methodology for Formal Analysis of Synthetic Biology Systems. IEEE/ACM Transactions on Computational Biology and Informatics. 2015. [Proposes a framework for formal analysis of synthetic biology systems, which includes use of PRISM for probabilistic model checking.]
[TTL14] Anton Tarasyuk, Elena Troubitsyna and Linas Laibinis. Integrating stochastic reasoning into Event-B development. Formal Aspects of Computing, 27, pages 53–77. 2015. [Describes an extension of Event-B for stochastic reasoning, using PRISM to perform probability calculations.]
[NS15] Bojan Nokovic and Emil Sekerinski. A Holistic Approach in Embedded System Development. In Proc. 2nd International Workshop on Formal Integrated Development Environment (F-IDE'15). 2015. [Presents pState, a tool for development of embedded systems, which uses PRISM for model analysis and verification.]
[CGJ+15] Radu Calinescu, Carlo Ghezzi, Kenneth Johnson, Mauro Pezzé, Yasmin Rafiq and Giordano Tamburrelli. Formal Verification With Confidence Intervals to Establish Quality of Service Properties of Software Systems. IEEE Transactions on Reliability. 2015. [Uses PRISM as part of a tool chain formally verify QoS properties of software systems.]
[CGLG15] Zack Coker, David Garlan and Claire Le Goues. SASS: Self-adaptation using stochastic search. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes the use of stochastic search techniques for self-adaptive systems, illustrated with a genetic algorithm that uses PRISM to compute fitness functions.]
[CGB15] Radu Calinescu, Simos Gerasimou and Alec Banks. Self-Adaptive Software with Decentralised Control Loops. In Proc. 18th International Conference on Fundamental Approaches to Software Engineering (FASE'15). 2015. [Presents an approach for decentralised control of self-adaptive systems, using PRISM as an underlying model checker.]
[NSG+15] Athanasios Naskos, Emmanouela Stachtiari, Anastasios Gounaris, Panagiotis Katsaros, Dimitrios Tsoumakos, Ioannis Konstantinou and Spyros Sioutas. Dependable Horizontal Scaling Based On Probabilistic Model Checking. In Proc. 15th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGrid'15). 2015. [Uses probabilistic model checking and PRISM for cloud elasticity, i.e. on-demand resource provisioning in cloud computing.]
[PLK+15] Jaime Pulido Fentanes, Bruno Lacerda, Tomas Krajnik, Nick Hawes and Marc Hanheide. Now or later? Predicting and Maximising Success of Navigation Actions from Long-Term Experience. In Proc. 2015 IEEE International Conference on Robotics and Automation (ICRA'14). 2015. [Proposes novel approaches to predicting changes in a robot's environment, applied to a probabilistic planning framework using PRISM as an underlying solver.]
[LMO15] Gabriele Lenzini, Sjouke Mauw and Samir Ouchani. Security Analysis of Socio-Technical Physical Systems. Computers & Electrical Engineering, Elsevier. 2015. [Proposes an approach to detect and quantify attacks in socio-technical physical systems, using a mapping to PRISM.]

2014

[CRJB14] Radu Calinescu, Yasmin Rafiq, Kenneth Johnson and Mehmet Emin Bakir . Adaptive Model Learning for Continual Verification of Non-Functional Properties. In Proc. 5th ACM/SPEC international conference on Performance engineering (ICPE'14), pages 87-98, ACM. 2014. [Proposes adaptive model learning techniques for continuous probabilistic verification, including PRISM as a backend solver.]
[GPST14] Carlo Ghezzi, Mauro Pezzè, Michele Sama and Giordano Tamburrelli. Mining Behavior Models from User-Intensive Web Applications. In Proc. ICSE'14. 2014. [Proposes techniques to infer probabilistic behaviour models from web application logs and analyses the models using PRISM.]
[RLK14] Pedro Rodrigues, Emil Lupu and Jeff Kramer. LTSA-PCA: tool support for compositional reliability analysis. In 36th International Conference on Software Engineering, ICSE '14, Companion Proceedings, pages 548-551. 2014. [Presents an extension of the LTSA model checker for compositional reliability analysis, which uses a connection to PRISM. ]
[KH14] Koichi Kobayashi and Kunihiko Hiraishi. Verification and Optimal Control of Context-Sensitive Probabilistic Boolean Networks Using Model Checking and Polynomial Optimization. The Scientific World Journal. 2014. [Presents various techniques for analysing probabilistic Boolean networks, including one that uses probabilistic model checking and PRISM.]
[SR14] Guoxin Su and David S. Rosenblum. Perturbation analysis of stochastic systems with empirical distribution parameters. In Proc. 36th International Conference on Software Engineering (ICSE'14). 2014. [Proposes techniques for analysing peturbations in probabilistic models using parametric model checking and a connection to PRISM.]
[LJ14] Nian-Ze Lee and Jie-Hong R. Jiang. Towards formal evaluation and verification of probabilistic design. In Proc. 2014 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'14). 2014. [Uses PRISM as part of a framework to verify approximate and probabilistic designs for circuits.]
[GCB14] Efficient Runtime Quantitative Verification using Caching, Lookahead, and Nearly-Optimal Reconfiguration. Simos Gerasimou, Radu Calinescu and Alec Banks.. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), pages 115-124. 2014. [Presents advances in runtime quantitative verification with an implementation that uses PRISM as a model checker.]
[HHJC14] Luke Herbert, Zaza Nadja Lee Hansen, Peter Jacobsen and Pedro Cunha. Evolutionary optimization of production materials workflow processes. In Proc. 8th International Conference on Digital Enterprise Technology (DET'14). 2014. [Presents evolutionary optimisation techniques for stochastic production processes, using PRISM as an underlying model checker.]
[SBE14] Khalid Sultan, Jamal Bentahar and Mohamed El-Menshawy. Model checking probabilistic social commitments for intelligent agent communication. Applied Soft Computing, 22, pages 397-409, Elsevier. 2014. [Performs probabilistic model checking of commitments in multi-agent systems via connection to PRISM.]
[OMD14] Samir Ouchani, Otmane Aït Mohameda and Mourad Debbabi. A property-based abstraction framework for SysML activity diagrams. Knowledge-Based Systems, 6, pages 328-343. January 2014. [Presents methods to abstract and verify SysML activity diagrams using PRISM as a back-end.]

2013

[CDF+13] Andrea Ciancone, Mauro Luigi Drago, Antonio Filieri, Vincenzo Grassi, Heiko Koziolek and Raffaela Mirandola. The KlaperSuite Framework for Model-Driven Reliability Analysis of Component-Based Systems. Software & Systems Modeling. 2013. [Describes the KlaperSuite framework for model-driven reliability analysis, which builds on several tools including PRISM.]
[KJR13] Radu Calinescu, Kenneth Johnson and Yasmin Rafiq. Developing Self-Verifying Service-Based Systems. In Proc. 28th IEEE/ACM International Conference on Automated Software Engineering (ASE'13), IEEE. 2013. [Describes a self-verifying framework for service-based systems, including PRISM as a backend solver.]
[SGO13] Simon Struck, Matthias Gudemann and Frank Ortmeier. Efficient Optimization of Large Probabilistic Models. Journal of Systems and Software. 2013. [Presents a framework for modelling, analysis and optimization of safety critical systems, which connects to PRISM.]
[ZREF13] Fokion Zervoudakis, David S. Rosenblum, Sebastian Elbaum and Anthony Finkelstein. Cascading Verification: An Integrated Method for Domain-Specific Model Checking. In Proc. 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE'13), pages 400-410 , ACM. 2013. [Proposes a domain-specific model checking framework, including PRISM as an underlying solver.]
[FBZ13] João Franco, Raul Barbosa and Mário Zenha Rela. Reliability analysis of software architecture evolution. In Proc. Latin-American Symposium on Dependable Computing (LADC'13). 2013. [Analyses quality attributes of software architectures by translating an architecture design language into PRISM. ]
[PTA13] Anna Philippou, Mauricio Toro and Margarita Antonaki. Simulation and Verification for a Process Calculus for Spatially-explicit Ecological Models. Scientific Annals of Computer Science, 23(1), pages 119–167. 2013. [Develops a stochastic process algebra for locations/populations called PALPS, with a translation into PRISM for probabilistic model checking.]
[JCK13] Kenneth Johnson, Radu Calinescu and Shinji Kikuchi. An Incremental Verification Framework for Component-Based Software Systems. In Proc. 16th International ACM Sigsoft symposium on Component-based software engineering (CBSE'13), pages 33-42. 2013. [Presents a framework for the efficient reverification of component-based software system, with a software prototype built on top of PRISM.]
[RBC+13] Neha Rungta, Guillaume Brat, William J. Clancey, Charlotte Linde, Franco Raimondi, Chin Seah and Michael Shafto. Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems. In Proc. International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
[HRRS13] Josie Hunter, Franco Raimondi, Neha Rungta and Richard Stocker. A synergistic and extensible framework for multi-agent system verification. In Proc. International conference on Autonomous Agents and Multi-Agent Systems (AAMAS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
[LFL13] Florian Leitner-Fischer and Stefan Leue. On the Synergy of Probabilistic Causality Computation and Causality Checking. In Proc. 20th International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 246-263, Springer. 2013. [Develops an approach for causality checking, which uses PRISM for some of the underlying computations.]
[PLSVS13] Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In Proc. 25th International Conference on Computer Aided Verification (CAV'13). 2013. [Develops techniques for verification of MDPs with convex uncertainties, implemented through an interface to PRISM.]
[HS13] Luke Herbert and Robin Sharp. Precise Quantitative Analysis of Probabilistic Business Process Model and Notation Workflows. J. Comput. Inf. Sci. Eng., 13(1). 2013. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows.]
[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.]

2012

[FBZ12] Joao M. Franco, Raul Barbosa and Mario Zenha-Rela. Automated Reliability Prediction from Formal Architectural Descriptions. In Proc. 2012 Joint Working IEEE/IFIP Conference on Software Architecture (WICSA) and European Conference on Software Architecture (ECSA). 2012. [Analyses quality attributes of software architectures by translating an architecture design language into PRISM.]
[RLB+12] Mikolaj Rybinski, Michal Lula, Pawel Banasik, Slawomir Lasota and Anna Gambin. Tav4SB: Integrating tools for analysis of kinetic models of biological systems. BMC Systems Biology, 6(25). 2012.
[KSBH12] Heiko Koziolek, Bastian Schlich, Steffen Becker and Michael Hauck. Performance and reliability prediction for evolving service-oriented software systems. Empirical Software Engineering. To appear. 2012.
[Kum12] Jayanand Asok Kumar. Statistical Guarantees of Performance for RTL Designs. Ph.D. thesis, University of Illinois at Urbana-Champaign. 2012. [bib]
[OGLS12] Frank Ortmeier, Matthias Gudemann, Michael Lipaczewski and Simon Struck. Unifying Probabilistic and Traditional Formal Model Based Analysis. In Proc. MBEES. 2012.
[GMS+12] Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe Ferri and Edson Watanabe. Constructive model-based analysis for safety assessment. International Journal on Software Tools for Technology Transfer (STTT). 2012. [Uses PRISM in a quantitative safety assessment framework via model translation from Simulink.]
[JD12] Yosr Jarraya and Mourad Debbabi. Formal Specification and Probabilistic Verification of SysML Activity Diagrams. In Proc. 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12). 2012. [Presents a framework for probabilistic verification of SysML activity diagrams via a translation to PRISM.]
[MMAG12] Indika Meedeniya, Irene Moser, Aldeida Aleti and Lars Grunske. Evaluating Probabilistic Models with Uncertain Model Parameters. Software and Systems Modelling, Springer. 2012. [Proposes techniques to evaluate probabilistic models with uncertainty, using PRISM as a back-end solution engine.]
[KG12] Christian Krause and Holger Giese. Probabilistic Graph Transformation Systems. In Proc. 6th International Conference on Graph Transformations (ICGT'12), pages 311-325. 2012. [Proposes techniques to analyse probabilistic graph transformation systems, using the tools HENSHIN and PRISM.]
[VK12] Mahsa Varshosaz and Ramtin Khosravi. Modeling and Verification of Probabilistic Actor Systems Using pRebeca. In Proc. 14th International Conference on Formal Engineering Methods, Formal Methods and Software Engineering (ICFEM'12), volume 7635 of LNCS, Springer. 2012. [Uses PRISM to analyse systems described in a probabilistic actor-based modelling language called pRebeca.]
[HS12] Luke Herbert and Robin Sharp. Using stochastic model checking to provision complex business services. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 98-105, IEEE. 2012. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows. Illustrated on a medical case study.]
[LSO12] Michael Lipaczewski, Simon Struck and Frank Ortmeier. Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 159-166. 2012. [Presents tool support for the safety analysis modelling language (SAML), which connects to PRISM for probabilistic verification.]
[SLOG12] Simon Struck, Michael Lipaczewski, Frank Ortmeier and Matthias Güdemann. Multi-objective Optimization of Formal Specifications. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 201-208. 2012. [Develops model-based optimisation methods which connect to PRISM for model analysis.]
[CGKM12] Radu Calinescu, Carlo Ghezzi, Marta Kwiatkowska and Raffaela Mirandola. Self-adaptive Software Needs Quantitative Verification at Runtime. Communications of the ACM, 55(9), pages 69-77, ACM. September 2012. [pdf] [bib] [Describes a framework for quantitative runtime verification that incorporates PRISM.]

2011

[LFL11] Florian Leitner-Fischer and Stefan Leue. QuantUM: Quantitative Safety Analysis of UML Models. In Proc. 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11). 2011. [bib]
[LMG11] Markus Lumpe, Indika Meedeniya and Lars Grunske. PSPWizard: Machine-assisted definition of temporal logical properties with specification patterns. In Proc. 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering and 13rd European Software Engineering Conference (ESEC/FSE'11), pages 468-471. 2011. [bib]
[GO11] Matthias Gudemann and Frank Ortmeier. Towards Model-driven Safety Analysis. In Proc. 3rd International Workshop on Dependable Control of Discrete Systems (DCDS'11). 2011.
[KLFL11] Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue. From Probabilistic Counterexamples via Causality to Fault Trees. In Proc. 30th International Conference on Computer Safety, Reliability, and Security (SAFECOMP'11). 2011.
[STTT11] Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi and Kazuko Takahashi. Probabilistic Symmetry Reduction for a System with Ring Buffer. IEICE Transactions, 94-D(5), pages 967-975. 2011. [bib]
[KLV11] Jayanand Asok Kumar, Lingyi Liu and Shobha Vasudevan. Scaling Probabilistic Timing Verification of Hardware Using Abstractions in Design Source Code. In Proc. 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD'11). 2011. [bib]
[JRC11] Kenneth Johnson, Simon Reed and Radu Calinescu. Specification and Quantitative Analysis of Probabilistic Cloud Deployment Patterns. In Proc. 7th Haifa Verification Conference (HVC'11). 2011. [bib]
[AB11] R. Abo and K. Barkaoui. A performability analysis of mobile wireless sensor networks with probabilistic model checking. In Proc. Wireless Advanced (WiAd'11), pages 283-288. 2011.
[KSB+11] Heiko Koziolek, Bastian Schlich, Carlos Bilich, Roland Weiss, Steffen Becker, Klaus Krogmann, Mircea Trifu, Raffaela Mirandola and Anne Martens. An Industrial Case Study on Quality Impact Prediction for Evolving Service-Oriented Software. In Proc. 33rd ACM/IEEE International Conference on Software Engineering (ICSE'11), pages 776-785, ACM. 2011.
[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.]
[CGKMT11] Radu Calinescu, Lars Grunske, Marta Kwiatkowska, Raffaela Mirandola and Giordano Tamburrelli. Dynamic QoS Management and Optimisation in Service-Based Systems. IEEE Transactions on Software Engineering, 37(3), pages 387-409. May 2011. [bib] [Presents a framework for developing adaptive service-based systems, using PRISM to compute QoS properties.]

2010

[RMH10] C. Rohr, W. Marwan and M. Heiner. Snoopy - A unifying Petri net framework to investigate biomolecular networks. Bioinformatics, 26(7), pages 974-975. 2010. [bib]
[ZYXL10] Yefei Zhao, Zongyuan Yang, Jinkui Xie and Qiang Liu. Quantitative Analysis of System Based on Extended UML State Diagrams and Probabilistic Model Checking. Journal of Software, 5(7), pages 793-800. 2010. [bib]
[AA10] M. Akbarzadeh and M. Azgomi. A framework for probabilistic model checking of security protocols using coloured stochastic activity networks and PDETool. In Proc. 5th International Symposium on Telecommunications (IST'10), pages 210-215. 2010. [bib]
[Jar10] Yosr Jarraya. Verification and Validation of UML and SysML Based Systems Engineering Design Models. Ph.D. thesis, Concordia University. 2010. [bib]
[HKL+10] B. Haverkort, M. Kuntz, F. Leitner-Fischer, A. Remke and S. Roolvink. Probabilistic Verification of Architectural Software Models using SoftArc and Prism. In Proc. ESREL Annual Conference. 2010. [bib]
[GO10b] Matthias Gudemann and Frank Ortmeier. A Framework for Qualitative and Quantitative Formal Model-Based Safety Analysis. In Proc. 12th IEEE High Assurance Systems Engineering Symposium (HASE'10), pages 132-141. 2010.
[CK10] Radu Calinescu and Marta Kwiatkowska. Software Engineering Techniques for the Development of Systems of Systems. In Christine Choppy and Oleg Sokolsky (editors), Proc. 15th Monterey Workshop on Foundations of Computer Software. Future Trends and Techniques for Development (Monterey'08), volume 6028 of LNCS, pages 59-82, Springer. September 2010. [pdf] [bib] http://www.springerlink.com/content/6334127431456134/ [Presents a framework for system-of-systems development, incorporating PRISM.]

2009

[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]
[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]
[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]
[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]
[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.]
[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] [Presents a tool chain for analysing Stochastic Reo models, incorporating PRISM.]
[CK09] R. Calinescu and M. Kwiatkowska. Using Quantitative Analysis to Implement Autonomic IT Systems. In Proc. 31st International Conference on Software Engineering (ICSE'09), pages 100-110, IEEE Press. May 2009. [pdf] [bib] [Presents an autonomic software framework, incorporating quantitative analysis of system models using PRISM.]
[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] [Presents a tool for developing self-* systems, based on Markov chain analysis using PRISM.]
[NPPW09] Gethin Norman, Catuscia Palamidessi, David Parker and Peng 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] [Presents model checking techniques for the probabilistic/stochastic pi-calculus based on a translation to PRISM.]

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

2007

[JSDH07] Yosr Jarraya, Andrei Soeanu, Mourad Debbabi and Fawzi Hassaine. Automatic Verification and Performance Analysis of Time-Constrained SysML Activity Diagrams. In Proc. 14th Annual IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'07), pages 515-522, IEEE. 2007. [bib]
[MM07] A. McIver and C. Morgan. Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic, 8(1). 2007. [bib]
[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] http://www.dcs.shef.ac.uk/~nw/Publications.html
[DAp07] D. D'Aprile. Timed and Stochastic Model Checking of Petri Nets. Ph.D. thesis, Dipartimento di Informatica, University of Torino. 2007. [bib] http://www.di.unito.it/~phd/documents/tesi/XIX/DAprileTesiJan2007.pdf
[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] http://www.itee.uq.edu.au/~grunske/Research/
[ABS+07] A. Abate, Y. Bai, N. Sznajder, C. Talcott and A. Tiwari. Quantitative and Probabilistic Modeling in Pathway Logic. In Proc. 7th IEEE International Conference on Bioinformatics and Bioengineering (BIBE'07). 2007. [bib]
[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.]
[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] 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.]
[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]

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]
[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]
[RCGB+06] Francisco José Romero-Campero, Marian Gheorghe, Luca Bianco, Dario Pescini, Mario J. Péerez-Jiménez and Rodica Ceterchi. Towards Probabilistic Model Checking on P Systems Using PRISM. In Workshop on Membrane Computing, pages 477-495. 2006.
[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] http://www.dcs.gla.ac.uk/people/personal/alice/publications.html
[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. http://fas.sfu.ca/pub/cs/techreports/2006/CMPT2006-02.pdf

2005

[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. http://www.cs.le.ac.uk/people/rh122/papers/2005/Hec05ICTAC.pdf
[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. http://www.sciencedirect.com/
[DM05] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Systems. In Proc. 12th workshop on Automated Reasoning, pages 17-18. July 2005. [bib] http://www.dcs.gla.ac.uk/people/personal/alice/publications.html
[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] http://www.di.unipi.it/~milazzo/
[GW05] M. Goldsmith and P. Whittaker. A CSP Frontend for Probabilistic Tools. Technical report FORWARD Deliverable D14, Formal Systems (Europe Ltd). June 2005. [bib] http://www.forward-project.org.uk/PDF_Files/D14.pdf

2004

[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] http://fakinf.informatik.unibw-muenchen.de/~msiegle/own.html
[Gol04] M. Goldsmith. CSP: The Best Concurrent-System Description Language in the World - Probably!. In Proc. Communicating Process Architectures (CPA'04). 2004. [bib] http://www.wotug.org/cpa2004/programme.shtml
[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] http://www.di.unipi.it/~milazzo/
[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. http://fakinf.informatik.unibw-muenchen.de/~msiegle/own.html
[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. http://www.dcs.ed.ac.uk/home/stg/
[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] http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3256&spage=210
[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. http://www.di.unito.it/~sproston/Research/research.html

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] http://www.mfn.unipmn.it/~bobbio/BIBLIO/bliagg.html
[Jan03] D. Jansen. Extensions of statecharts with probability, time, and stochastic timing. Ph.D. thesis, Universiteit Twente. October 2003. http://depend.cs.uni-sb.de/?id=200
[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. http://www.cs.iastate.edu/~leavens/SAVCBS/2003/papers/index.shtml
[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. http://www.dcs.ed.ac.uk/home/stg/
[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. http://www.dcs.ed.ac.uk/home/stg/

2002

[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. http://depend.cs.uni-sb.de/?id=200

PRISM tool papers

2020

[BHK+20] Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretinsky, David Parker, Tim Quatmann, Andrea Turrini and Zhen Zhang. On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report. In Proc. 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'20), Springer. To appear. October 2020. [pdf] [bib] [Summarises the 2020 Comparison of Tools for the Analysis of Quantitative Formal Models (QComp'20) featuring PRISM and 8 other tools.]
[KNPS20] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 475-487, Springer. July 2020. [pdf] [bib] [Tool paper describing the new features in PRISM-games 3.0.]

2019

[HHH+19] Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Křetínský, David Parker, Tim Quatmann, Enno Ruijters and Marcel Steinmetz. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models (QComp 2019 Competition Report). In Proc. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11429 of LNCS, pages 69-92, Springer. April 2019. [pdf] [bib] [Summarises the first Quantitative Formal Models competition (QComp) featuring PRISM and 8 other tools.]
[HKPQR19] Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann and Enno Ruijters. The Quantitative Verification Benchmark Set. In Proc. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), volume 11427 of LNCS, pages 344-350, Springer. April 2019. [pdf] [bib] [Presents a benchmark suite for quantitative verification, include a selection of models/properties for use in PRISM.]

2018

[KPW18] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games: Verification and Strategy Synthesis for Stochastic Multi-player Games with Multiple Objectives. International Journal on Software Tools for Technology Transfer, 20(2), pages 195–210, Springer. April 2018. [pdf] [bib] [Provides a detailed overview of PRISM-games, including its modelling and property specification formalisms, underlying architecture and implementation, experimental results and case studies.]

2016

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

2013

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

2011

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

2006

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

2004

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

2002

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

2001

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

PRISM-related tutorials and surveys

2017

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

2016

[Kwi16] Marta Kwiatkowska. Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice. In Proc. 43rd International Colloquium on Automata, Languages, and Programming (ICALP'16), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2016. [bib] [Gives an overview of quantitative verification and strategy synthesis for stochastic multi-player games, as implemented in PRISM-games.]
[SK16] Maria Svorenova and Marta Kwiatkowska. Quantitative Verification and Strategy Synthesis for Stochastic Games. European Journal of Control, Elsevier. To appear. 2016. [pdf] [bib] [Provides an overview of techniques for quantitative verification and strategy synthesis for stochastic games.]

2014

[KT14] Marta Kwiatkowska and Chris Thachuk. Probabilistic Model Checking for Biology. In Software Safety and Security, IOS Press. 2014. [pdf] [bib] [A tutorial on the application of probabilistic model checking and PRISM to biological systems, including examples of DNA computation.]

2013

[Kwi13] Marta Kwiatkowska. From Software Verification to 'Everyware' Verification. Computer Science - Research and Development, 28(4), pages 295-310, Springer. November 2013. [pdf] [bib] [Summarises ongoing research into verification of 'everyware', including techniques and tools that improve, extend and connect to PRISM.]
[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.]
[NPS13] Gethin Norman, David Parker and Jeremy Sproston. Model Checking for Probabilistic Timed Automata. Formal Methods in System Design, 43(2), pages 164-190, Springer. September 2013. [pdf] [bib] [Survey/tutorial paper on probabilistic timed automata and techniques for their verification, and two illustrative case studies.]
[Kwi13b] Marta Kwiatkowska. Advances in Quantitative Verification for Ubiquitous Computing. In Proc. 10th International Colloquium on Theoretical Aspects of Computing (ICTAC'13), volume 8049 of LNCS, pages 42-58, Springer. September 2013. [pdf] [bib] [Invited paper on recent developments in quantitative verification for ubiquitous computing, illustrated by three PRISM case studies. ]

2012

[Kwi12] Marta Kwiatkowska. Sensing Everywhere: Towards Safer and More Reliable Sensor-enabled Devices. In Proc. 31st International Conference on Computer Safety, Reliability and Security (SAFECOMP'12), Springer. September 2012. [pdf] [bib] [Invited talk on research directions for verification of sensor-enabled devices, including PRISM-based analyses.]
[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.]

2011

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

2010

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

2009

[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).]
[KNP09a] Marta Kwiatkowska, Gethin Norman and David 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] [Provides an overview of PRISM and its application to performance and and reliability analysis.]

2008

[KNP08a] Marta Kwiatkowska, Gethin Norman and David 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] [Illustrates the applicability of PRISM to systems biology, using a case study: the 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.]

2007

[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] [Overview of probabilistic model checking and PRISM, with a particular emphasis on DTMCs.]
[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.]

2004

[KNP04a] Jan Rutten, Marta Kwiatkowska, Gethin Norman and David 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]

2003

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

Others

2020

[Eva20] Alexandros Evangelidis. Verified Control and Estimation for Cloud Computing. Ph.D. thesis, School of Computer Science, University of Birmingham. June 2020. [pdf] [bib] [Proposes techniques and tools for formal analysis of resource control and estimation mechanisms in cloud computing, building on probabilistic model checking and PRISM.]
[OPR20] Michael Oxford, David Parker and Mark Ryan. Quantitative Verification of Certificate Transparency Gossip Protocols. In Proc. 6th International Workshop on Security and Privacy in the Cloud (SPC'20), IEEE. To appear. June 2020. [pdf] [bib] [Analyses the effectiveness of certificate transparency gossiping protocols using probabilistic model checking and PRISM.]

2019

[PFF+19] Avi Pfeffer, Curt Wu, Gerald Fry, Kenny Lu, Steve Marotta, Mike Reposa, Yuan Shi, T. K. Satish Kumar, Craig A. Knoblock, David Parker, Irfan Muhammad and Chris Novakovic. Software Adaptation for an Unmanned Undersea Vehicle. IEEE Software, 36(2), pages 91-96, IEEE. March 2019. [pdf] [bib] [Summarises the PRINCESS project, which develops methods for adapting an optimising software at runtime, including mission verification using extensions of PRISM.]

2016

[IQV16] Paolo Izzo, Hongyang Qu and Sandor M. Veres. A stochastically verifiable autonomous control architecture with reasoning. In Proc. IEEE Conference on Decision and Control (CDC'16). 2016. [Proposes an architecture for autonomous control with underlying verification abilities provided by 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.]

2014

[HBHS14] Fenglin Han, Jan Olaf Blech, Peter Herrmann and Heinz Schmidt. Towards Verifying Safety Properties of Real-Time Probabilistic Systems. In Proc. Formal Engineering Approaches to Software Components and Architectures (FESCA'14), EPTCS. 2014. [Presents an extension of the Reactive Blocks tool set for analysing probabilistic real-time systems, through a connection to PRISM.]
[DHK14] Frits Dannenberg, Ernst Moritz Hahn and Marta Kwiatkowska. Computing Cumulative Rewards using Fast Adaptive Uniformisation. ACM Transactions on Modeling and Computer Simulation, Special Issue on Computational Methods in Systems Biology. 2014. [pdf] [bib] [Develops fast adaptive uniformisation techniques for cumulative reward properties, implemented in PRISM.]
[JD14] Yosr Jarraya and Mourad Debbabi. Quantitative and qualitative analysis of SysML activity diagrams. International Journal on Software Tools for Technology Transfer, 16(4), pages 399-419. 2014. [Presents a framework for probabilistic verification of SysML activity diagrams via a translation to PRISM.]
[NP14] Gethin Norman and David Parker. Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. A report by the London Mathematical Society and the Smith Institute. Edited by Robert Leese and Tom Melham. 2014. [pdf] [bib] [Gives a short, accessible introduction to quantitative verification, with a focus on model checking for timed and probabilistic systems.]
[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.]
[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.]

2012

[BDE+12b] Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code. In Proc. 7th Conference on Systems Software Verification (SSV'12), volume 102 of EPTCS. 2012. [Investigates symmetry reduction techniques for probabilistic model checking using models build with 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.]

2011

[CFCC11] Mirlaine A Crepalde, Alessandra C Faria-Campos and Sérgio VA Campos. Modeling and analysis of cell membrane systems with probabilistic model checking. BMC Genomics, 12(Suppl 4)(S14). 2011. [Analyses a sodium-potassium exchange pump using probabilistic model checking and PRISM.]

2006

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

2004

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

2003

[MPK03a] Rashid Mehmood, David Parker and Marta 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]

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

2000

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

Sort by: date, type, title, subject