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

779 publications:

2023

[SD23] Ramesh Kumar Shanmugam and Tarun Dhingra. Outcome-based contracts - Linking technology, ownership and reputations. International Journal of Information Management, 70. 2023. [Uses probabilistic model checking and PRISM-games to analyse outcome-based contracts for information technology outsourcing. ]
[BRA+23] Thom Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A. Poonawala, Marielle Stoelinga and Nils Jansen. Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions. Journal of Artificial Intelligence Research, 76, pages 341-391. January 2023. [pdf] [bib] [Presents methods to synthesise controllers, with probabilistic guarantees obtained using an extension of PRISM for IMDPs.]

2022

[LP22] Alessio Lomuscio and Edoardo Pirovano. A counter abstraction technique for verifying properties of probabilistic swarm systems. Artificial Intelligence, 305. 2022. [Presents techniques for verification of probabilistic swarm systems developed as an extension of PRISM. ]
[Bac22] Edoardo Bacci. Formal Verification of Deep Reinforcement Learning Agents. Ph.D. thesis, School of Computer Science, University of Birmingham. 2022. [pdf] [bib] [Proposes several techniques for verification of deep reinforcement learning policies, with implementations building upon PRISM. ]
[Far22] Fatma Faruq. Verified Multi-Robot Planning Under Uncertainty. Ph.D. thesis, School of Computer Science, University of Birmingham. 2022. [pdf] [bib] [Develops various methods for synthesising verified multi-robot policies, with an implementation built on top of PRISM. ]
[RB22b] Kaustabha Ray and Ansuman Banerjee. Preference-Aware Computation Offloading for IoT in Multi-Access Edge Computing Using Probabilistic Model Checking. In Proc. 19th International Conference on Quantitative Evaluation of SysTems (QEST'22), Springer. 2022. [Uses probabilistic model checking and PRISM-games to generate policies for Multi-Access Edge Computing.]
[EWT22] Khalil Esper, Stefan Wildermann and Jürgen Teich. Multi-Requirement Enforcement of Non-Functional Properties on MPSoCs Using Enforcement FSMs - A Case Study. In Proc. 3rd Workshop on Next Generation Real-Time Embedded Systems (NG-RES@HiPEAC). 2022. [Tackles embedded system control problems using probabilistic model checking and PRISM.]
[YCF+22] Kangfeng Ye, Ana Cavalcanti, Simon Foster, Alvaro Miyazawa and Jim Woodcock. Probabilistic modelling and verification using RoboChart and PRISM. Software and Systems Modeling, 21, pages 667–716, Springer. 2022. [Presents a probabilistic extension to the RoboChart language with tool support building on PRISM.]
[RB22a] Kaustabha Ray and Ansuman Banerjee. Prioritized Fault Recovery Strategies for Multi-Access Edge Computing Using Probabilistic Model Checking. IEEE Transactions on Dependable and Secure Computing. 2022. [Uses PRISM-games combined with heuristics to generate fault-recovery strategies for Multi-Access Edge Computing.]
[SKH+22] Jiyoung Song, Jeehoon Kang, Sangwon Hyun, Eunkyoung Jee and Doo-Hwan Bae. Continuous verification of system of systems with collaborative MAPE-K pattern and probability model slicing. Information and Software Technology, 147, Elsevier. 2022. [Proposes methods for continuous-verification-of-SoS including modelling and analysis with PRISM.]
[Ray22] Kaustabha Ray. Policy Design and Verification for Multi-Access Edge Computing: A Formal Methods Perspective. Ph.D. thesis, Indian Statistical Institute, Kolkata. 2022. [Presents verification techniques for multi-access edge computing, building upon PRISM and PRISM-games.]
[KNPS22b] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games. In Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of LNCS, Springer. December 2022. [pdf] [bib] [Investigates symbolic model checking of turn-based stochastic games, implemented in PRISM-games.]
[SSJP22] Marnix Suilen, Thiago D. Simão, Nils Jansen and David Parker. Robust Anytime Learning of Markov Decision Processes. In Proc. 36th Annual Conference on Neural Information Processing Systems (NeurIPS'22). To appear. November 2022. [pdf] [bib] [Proposes a robust, anytime approach to learning MDPs, with an implementation building on PRISM's support for IMDPs.]
[SPH+22] Shili Sheng, Erfan Pakdamanian, Kyungtae Han, Ziran Wang, John Lenneman, David Parker and Lu Feng. Planning for Automated Vehicles with Human Trust. ACM Transactions on Cyber-Physical Systems. To appear. September 2022. [pdf] [bib] [Proposes a trust-based route planning approach for automated vehicles, with an implementation that builds upon PRISM's support for POMDPs.]
[YSD+22] Rui Yan, Gabriel Santos, Xiaoming Duan, David Parker and Marta Kwiatkowska. Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Games. In Proc. 38th Conference on Uncertainty in Artificial Intelligence (UAI'22), Proceedings of Machine Learning Research 180. August 2022. [pdf] [bib] [Develops methods for finite-horizon analysis of neuro-symbolic concurrent stochastic games, implemented on top of PRISM-games.]
[KNP+22] Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. In Proc. 47th International Symposium on Mathematical Foundations of Computer Science (MFCS'22), pages 4:1-4:22. August 2022. [pdf] [bib] [Provides an overview of recent work developing a modelling and verification framework using concurrent stochastic games.]
[CBPF22] Shenghui Chen, Kayla Boggess, David Parker and Lu Feng. Multi-Objective Controller Synthesis with Uncertain Human Preferences. In Proc. ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS'22), pages 170-180, IEEE. May 2022. [pdf] [bib] [Develops techniques for multi-objective MDP controller synthesis over uncertain preferences, implemented in an extension of PRISM.]
[BP22] Edoardo Bacci and David Parker. Verified Probabilistic Policies for Deep Reinforcement Learning. In Proc. 14th International Symposium NASA Formal Methods (NFM'22), volume 13260 of LNCS, pages 193-212, Springer. May 2022. [pdf] [bib] [Presents techniques to produce formal guarantees on the safe execution of probabilistic policies for deep reinforcement learning, building on PRISM's model checking engines.]
[KNP22] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking and Autonomy. Annual Review of Control, Robotics, and Autonomous Systems, 5, pages 385-410, Annual Reviews. May 2022. [pdf] [bib] [Gives an overview of probabilistic model checking as applied to the context of robotics and autonomous systems.]
[KNPS22] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Correlated Equilibria and Fairness in Concurrent Stochastic Games. In Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22), volume 13244 of LNCS, pages 60–78, Springer. April 2022. [pdf] [bib] [Presents novel techniques for synthesising equilibria in stochastic games, implemented in PRISM-games.]
[BAJ+22] Thom S. Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A. Poonawala and Marielle Stoelinga. Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise. In Proc. 36th AAAI Conference on Artificial Intelligence (AAAI'22), pages 9669-9678. Distinguished Paper Award. March 2022. [pdf] [bib] [Presents methods to synthesise controllers, with probabilistic guarantees obtained using an extension of PRISM for IMDPs.]

2021

[FCD+21] Syyeda Zainab Fatmi, Xiang Chen, Yash Dhamija, Maeve Wildes, Qiyi Tang and Franck van Breugel. Probabilistic Model Checking of Randomized Java Code. In Proc. 27th International Symposium on Model Checking Software (SPIN'21), volume 12864 of LNCS, pages 157-174, Springer. 2021. [Presents methods for probabilistic model checking of randomised Java code using a combination of PRISM and Java PathFinder.]
[SMAM21] Khayyam Salehi, Ali A. Noroozi and Sepehr Amir-Mohammadian. Quantifying Information Leakage of Probabilistic Programs Using the PRISM Model Checker. In Proc. 15th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE'21). 2021. [Develops methods for quantifying information leakage built into an extension of PRISM.]
[RB21b] Kaustabha Ray and Ansuman Banerjee. A Framework for Analyzing Resource Allocation Policies for Multi-Access Edge Computing. In Proc. IEEE International Conference on Edge Computing (EDGE'21), pages 102-110, IEEE. 2021. [Uses PRISM-games to verify resource allocation policies for multi-access edge computing. ]
[SYBG21] Qi Shao, Shunkun Yang, Chong Bian and Xiaodong Gou. Formal Analysis of Repairable Phased-Mission Systems With Common Cause Failures. IEEE Transactions on Reliability. 2021. [Proposes methods for reliability analysis of phased-mission systems, building on probabilistic model checking and PRISM.]
[JAA+21] Sascha Jung, Evan Appleton, Muhammad Ali, George M. Church and Antonio del Sol. A computer-guided design tool to increase the efficiency of cellular conversions. Nature Communications, 12. 2021. [Introduces a computer-guided design tool for cell conversion, including the use of PRISM for underlying computations.]
[SPM+21] Charlie Street, Sebastian Putz, Manuel Muhlig, Nick Hawes and Bruno Lacerda. Congestion-Aware Policy Synthesis for Multi-Robot Systems. IEEE Transactions on Robotics. 2021. [Proposes a congestion-aware multi-robot planning framework, with use of PRISM as an underlying solver.]
[ALMS21] Alessandro Aldini, Antonio La Marra, Fabio Martinelli and Andrea Saracino. Ask a(n)droid to tell you the odds: probabilistic security-by-contract for mobile devices. Soft Computing, 25, pages 2295–2314, Springer. 2021. [Proposes a probabilistic security-by-contract paradigm, including the use of probabilistic model checking and PRISM.]
[Spr21] Jeremy Sproston. Probabilistic Timed Automata with Clock-Dependent Probabilities. Fundamenta Informaticae, 178(1-2), pages 101-138, IOS Press. 2021. [Develops techniques for PTAs in which transition probabilities can depend on clocks, including experiments performed using PRISM.]
[CWC21] Jianyi Cheng, John Wickerson and George A. Constantinides. Probabilistic Scheduling in High-Level Synthesis. In Proc. IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM'21). 2021. [Presents probabilistic scheduling techniques for high-level synthesis, including the use of PRISM for probabilistic model analysis. ]
[WKL+21] Andrew M. Wells, Zachary Kingston, Morteza Lahijanian, Lydia E. Kavraki and Moshe Y. Vardi. Finite-Horizon Synthesis for Probabilistic Manipulation Domains. In Proc. IEEE International Conference on Robotics and Automation (ICRA'21). 2021. [Presents probabilistic synthesis techniques for collaborative human-robot manipulation tasks with an implementation that uses PRISM.]
[NKA21] Mehran Alidoost Nia, Mehdi Kargahi and Alessandro Abate. Resilient Monitoring in Self-Adaptive Systems through Behavioral Parameter Estimation. Journal of Systems Architecture. 2021. [Presents model-based techniques for self-adaptive systems, using PRISM for model verification.]
[RB21] Kaustabha Ray and Ansuman Banerjee. Modeling and Verification of Service Allocation Policies for Multi-Access Edge Computing Using Probabilistic Model Checking. IEEE Transactions on Network and Service Management. 2021. [Uses PRISM-games to model and verify service allocation policies for multi-access edge computing.]
[VSBH21] Heribert Vallant, Branka Stojanović, Josip Božić and Katharina Hofer-Schmitz. Threat Modelling and Beyond-Novel Approaches to Cyber Secure the Smart Energy System. Applied Sciences. 2021. [Proposes a threat model for smart grid, performing a risk analysis using PRISM.]
[GKL21] Romulo Meira-Goes, Raymond H. Kwong and Stephane Lafortune. Synthesis of optimal multi-objective attack strategies for controlled systems modeled by probabilistic automata. IEEE Transactions on Automatic Control. 2021. [Considers multi-objective synthesis of attack strategies using MDP models and solution via PRISM.]
[EWT21] Khalil Esper, Stefan Wildermann and Jürgen Teich. Enforcement FSMs: specification and verification of non-functional properties of program executions on MPSoCs. In Proc. 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'21). 2021. [Tackles embedded system control problems using probabilistic model checking and PRISM.]
[Pir21] Edoardo Pirovano. Parameterised model checking of probabilistic multi-agent systems. Ph.D. thesis, Imperial College London. 2021. [Develops techniques for probabilistic verification of swarm robotics, implemented in a tool PSV which builds on top of PRISM.]
[ZZdA+21] Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson and Limin Jia. Netter: Probabilistic, Stateful Network Models. In Proc. 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'21). 2021. [Presents a tool for analysis of probabilistic network models, using PRISM as a backend solver.]
[BMOB21] Abdelhakim Baouya, Otmane Ait Mohamed, Samir Ouchani and Djamal Bennouar. Reliability-driven Automotive Software Deployment based on a Parametrizable Probabilistic Model Checking. Expert Systems with Applications. 2021. [Presents techniques for analysing embedded systems specified in SysML via a translation to PRISM.]
[TPNP21] Polyxeni Tsompanoglou,Sophia Petridou,Petros Nicopolitidis and Georgios Papadimitriou. Quantitative model checking for assessing the energy impact of a MITM attack on EPONs. Internet Technology Letters. 2021. [Analyses man in the middle attacks on Ethernet Passive Optical Networks (EPONs) using probabilistic model checking and PRISM.]
[SAM21] Gautham Nayak Seetanadi, Karl-Erik Årzen and Martina Maggio. Control-based event-driven bandwidth allocation scheme for video-surveillance systems. Cyber-Physical Systems. 2021. [Analyses the performance and safety of video surveillance networks using PRISM.]
[KM20] William Kavanagh and Alice Miller. Gameplay Analysis of Multiplayer Games with Verified Action‐Costs. The Computer Games Journal, 10, pages 89-110. 2021. [bib] [Proposes techniques for measuring the skill levels of players in a game, including the use of PRISM-games.]
[DKT21] Clemens Dubslaff, Patrick Koopmann and Anni-Yasmin Turhan. Enhancing probabilistic model checking with ontologies. Formal Aspects of Computing. 2021. [Presents an ontology-mediated approach to probabilistic model checking, building upon PRISM for the implementation. ]
[ST21] Georg Friedrich Schuppe and Jana Tumova. Decentralized Multi-Agent Strategy Synthesis under LTLf Specifications via Exchange of Least-Limiting Advisers. In Proc. 2021 International Symposium on Multi-Robot and Multi-Agent Systems (MRS), pages 119-127. 2021. [Proposes techniques for multi-agent task-planning implemented in a tool chain incorporating PRISM-games.]
[BARI21] Borja Bordel, Ramon Alcarria, Tomas Robles and Marcos Sanchez Iglesias. Data Authentication and Anonymization in IoT Scenarios and Future 5G Networks Using Chaotic Digital Watermarking. IEEE Access, 9, pages 22378-22398. 2021. [Proposes an IoT authentication and anonymisation scheme and verifies it using PRISM.]
[VCC21] Gricel Vazquez, Radu Calinescu and Javier Camara. Scheduling Multi-robot Missions with Joint Tasks and Heterogeneous Robot Teams. In Proc. Annual Conference Towards Autonomous Robotic Systems (TAROS'21), pages 354-359. 2021. [Presents an approach to multi-robot scheduling, with a tool chain that includes PRISM for robot plan generation.]
[AZP+21] Iffat Anjum, Mu Zhu, Isaac Polinsky, William Enck, Michael K. Reiter and Munindar P. Singh. Role-Based Deception in Enterprise Networks. In Proc. 11th ACM Conference on Data and Application Security and Privacy (CODASPY'21), pages 65–76. 2021. [Develops a technique for deceiving adversaries in enterprise networks, and evaluates its security using PRISM.]
[DABB21] Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci and Borzoo Bonakdarpour. HyperProb: A Model Checker for Probabilistic Hyperproperties. In Proc. 24th International Symposium on Formal Methods (FM'21). 2021. [Presents a tool for verifying probabilistic hyperproperties on Markov Decision Processes represented in the PRISM modelling language.]
[WR21] Ke Coby Wang and Michael K. Reiter. Using Amnesia to Detect Credential Database Breaches. In Proc. 30th USENIX Security Symposium (USENIX Security 2021). 2021. [Presents a framework for detecting breaches in credential databases, using PRISM to quantify security.]
[YMCM21] Cangzhou Yuan, Kangzhao Wu, Guotao Chen and Yongjia Mo. An Automatic Transformation Method from AADL Reliability Model to CTMC. In Proc. IEEE International Conference on Information Communication and Software Engineering (ICICSE'21). 2021. [Presents methods for translating the AADL modelling language, using PRISM.]
[DHB21] Jacob Dineen, A. S. M. Ahsan-Ul Haque and Matthew Bielskas. Formal Methods for an Iterated Volunteer’s Dilemma. In Proc. International Conference on Social Computing, Behavioral-Cultural Modeling and Prediction and Behavior Representation in Modeling and Simulation (SBP-BRiMS'21). 2021. [Performs a formal analysis of the iterated volunteer’s dilemma using PRISM-games.]
[MSG21] Maria Maximova, Sven Schneider and Holger Giese. Interval Probabilistic Timed Graph Transformation Systems. In Proc. 14th International Conference on Graph Transformation (ICGT'21). 2021. [Presents the the formalism of Interval Probabilistic Timed Graph Transformation Systems, including connections to PRISM. ]
[Nie21] Florian Niedermeier. Power-Adaptive Computing in Future Energy Networks. Ph.D. thesis, University of Passau. 2021. [Presents methods for power-adaptive computing, including an analysis with PRISM.]
[GZSS21] Sagarika Ghosh, Marzia Zaman, Gary Sakauye and Srinivas Sampalli. An Intrusion Resistant SCADA Framework Based on Quantum and Post-Quantum Scheme. Applied Sciences. 2021. [Proposes an intrusion resistant quantum algorithm and analyses it using PRISM.]
[KNPS21] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Automatic Verification of Concurrent Stochastic Systems. Formal Methods in System Design, 58, pages 188–250, Springer. 2021. [pdf] [bib] [Proposes verification techniques for concurrent stochastic games, and implements and evaluates them in an extension of PRISM-games. ]
[DJK+21] Kalyani Dole, Ashutosh Gupta, John Komp, Shankaranarayanan Krishna and Ashutosh Trivedi. Event-Triggered and Time-Triggered Duration Calculus for Model-Free Reinforcement Learning. In Proc. IEEE Real-Time Systems Symposium (RTSS'21). 2021. [Presents reinforcement learning techniques that include an environment modelled using PRISM.]
[Oxf21] Michael Oxford. Quantitative Verification of Gossip Protocols for Certificate Transparency. Ph.D. thesis, School of Computer Science, University of Birmingham. April 2021. [pdf] [bib] [Studies gossip protocols for certificate transparency, using PRISM model models and a variety of new verification techniques.]
[San21] Gabriel Santos. Automatic Verification and Strategy Synthesis for Zero-sum and Equilibria Properties of Concurrent Stochastic Games. Ph.D. thesis, Department of Computer Science, University of Oxford. March 2021. [pdf] [bib] [Develops a variety of verification and strategy synthesis techniques for concurrent stochastic games, implemented in PRISM-games.]
[EP21] Alexandros Evangelidis and David Parker. Quantitative Verification of Kalman Filters. Formal Aspects of Computing, 33(4-5), pages 669-693, Springer. February 2021. [pdf] [bib] [Builds a framework for quantitative verification of Kalman filters on top of PRISM. ]

2020

[DMBJ20] Clemens Dubslaff, Andrey Morozov, Christel Baier and Klaus Janschek. Iterative Variable Reordering: Taming Huge System Families. In Proc. MARS'20, volume 316 of EPTCS, pages 121-133. 2020. [Presents novel symbolic model checking techniques for families of models, building on PRISM.]
[CKWW20] Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger and Tobias Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 398-420, Springer. 2020. [bib] [Develops a solving lexicographic reachability-safety objectives on stochastic games, implemented as an extension of PRISM-games.]
[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.]
[WLKV20] Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki and Moshe Y. Vardi. LTL_f Synthesis on Probabilistic Systems. In Proc. Int’l Symposium on Games, Automata, Logics, and Formal Verification (GandALF'20). 2020. [Presents techniques for finite-trace LTL and MDPs, with an implementation built on PRISM.]
[LV20] Cosimo Laneve and Adele Veschetti. A Formal Analysis of the Bitcoin Protocol. In Recent Developments in the Design and Implementation of Programming Languages. 2020. [Analyses Nakamoto’s Bitcoin protocol using an extension of PRISM.]
[CBDK20] Philipp Chrszon, Christel Baier, Clemens Dubslaff and Sascha Klüppelholz. From Features to Roles. In Proc. 24th ACM Conference on Systems and Software Product Line (SPLC'20). 2020. [Proposes verification techniques for feature-oriented systems, with a translation to PRISM for applying model checking.]
[Tak20] Ryuichi Takahashi. Evaluation the Redundancy of the IoT System Based on Individual Sensing Probability. IEICE Transactions on Information and Systems. 2020. [Evaluates the reliability of IoT systems via a translation to PRISM.]
[JHFB20] Simon Jantsch, Hans Harder, Florian Funke and Christel Baier. SWITSS: Computing Small Witnessing Subsystems. In Proc. Formal Methods in Computer Aided Design (FMCAD'20). 2020. [Proposes a tool for computing witnesses in Markov models, with underlying of PRISM for model generation.]
[DFT20] Rayna Dimitrova, Bernd Finkbeiner and Hazem Torfah. Probabilistic Hyperproperties of Markov Decision Processes. In Proc. 18th International Symposium on Automated Technology for Verification and Analysis (ATVA 2020). 2020. [Presents methods for model checking hyperproperties on Markov decision processes, with an implementation that uses PRISM to verify Markov chains.]
[WWA+20] Matt Webster, David G. Western, Dejanira Araiza-Illan, Clare Dixon, Kerstin Eder, Michael Fisher and Anthony G. Pipe. A corroborative approach to verification and validation of human–robot teams. International Journal of Robotics Research, 39(1). 2020. [Presents an approach for the verification and validation of robot assistants including the use of model checking with PRISM.]
[NSZD20] Jordi Navarrette, Subash Shankar, Xiaojie Zhang and Saptarshi Debroy. Formal Modeling and Analysis of Multi-Rogue Backoff Manipulation Attacks in Unlicensed Networks. In Proc. 16th International Conference on the Design of Reliable Communication Networks (DRCN'20), IEEE. 2020. [Analyses multi-rogue backoff manipulation attack strategies in secondary wireless networks using probabilistic model checking and PRISM.]
[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.]
[IIZ20] Azlan Ismail, Susanti Intu and Suzana Zambri. A GUI-driven prototype for synthesizing self-adaptation decision. Bulletin of Electrical Engineering and Informatics. 2020. [Proposes a decision-making approach for self-adapative systems implemented on top 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.]
[Gle20] Mario Gleirscher. YAP: Tool Support for Deriving Safety Controllers from Hazard Analysis and Risk Assessments. In Proc. 2nd Workshop on Formal Methods for Autonomous Systems (FMAS'20). 2020. [Presents a tool for formal risk analysis including modelling and verification support from PRISM.]
[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.]
[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.]
[LCGS20] Nianyu Li, Javier Cámara, David Garlan and Bradley Schmerl. Reasoning about When to Provide Explanation for Human-involved Self-Adaptive Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20). 2020. [Reasons about self-adaptive systems with human involvement using probabilistic model checking and PRISM-games.]
[GGS20] T. J. Glazier, D. Garlan and B. Schmerl. Automated Management of Collections of Autonomic Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20), pages 82-91. 2020. [Proposes an automated approach to managing multiple autonomic systems, building upon PRISM-games. ]
[KSHB20] Shamik Kundu, Ahmet Soyyiğit, Khaza Anuarul Hoque and Kanad Basu. High-level Modeling of Manufacturing Faults in Deep Neural Network Accelerators. In Proc. IEEE 26th International Symposium on On-Line Testing and Robust System Design (IOLTS'20). 2020. [Formally models and analyses faults in deep neural network accelerators using probabilistic model checking and PRISM.]
[MKI20] Mohammadsadegh Mohagheghi, Jaber Karimpour and Ayaz Isazadeh. Prioritizing Methods to Accelerate Probabilistic Model Checking of Discrete-Time Markov Models. The Computer Journal, 63(1), pages 105–122. 2020. [Proposes efficiency improvements for solving Markov decision processes, implemented as an extension of PRISM.]
[MS20] MohammadSadegh Mohagheghi and Khayyam Salehi. Accelerating Interval Iteration for Expected Rewards in Markov Decision Processes. In Proc. 15th International Conference on Software Technologies (ICSOFT'20), pages 39-50. 2020. [Proposes efficient iterative methods for solving Markov decision processes, implemented as an extension of PRISM. ]
[LP20] Alessio Lomuscio and Edoardo Pirovano. Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. In Proc. 19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'20), pages 762-770. 2020. [Develops techniques and a tool for verifying parameterised probabilistic multi-agent systems, building upon PRISM and PRISM-games.]
[LP20b] Alessio Lomuscio and Edoardo Pirovano. Verifying Fault-Tolerance in Probabilistic Swarm Systems. In Proc. 29th International Joint Conference on Artificial Intelligence (IJCAI'20), pages 325-331. 2020. [Presents techniques for formally analysing fault-tolerance in unbounded robotic swarms, with an implementation that builds on PRISM.]
[XKSS20] Xin Xin, Sye Loong Keoh, Michele Sevegnani and Martin Saerbeck. Dynamic Probabilistic Model Checking for Sensor Validation in Industry 4.0 Applications. In Proc. IEEE International Conference on Smart Internet of Things (IEEE SmartIoT 2020), pages 43-50. 2020. [Proposes a run-time verification framework for sensor networks based on probabilistic model checking and PRISM.]
[BMMK20] Abul Bashar, Shahabuddin Muhammad, Nazeeruddin Mohammad and Majid Khan. Modeling and Analysis of MDP-based Security Risk Assessment System for Smart Grids. In Proc. 2020 Fourth International Conference on Inventive Systems and Control (ICISC). 2020. [Designs a security risk management solution for smart grids, analysed using PRISM.]
[MMAM20] Tariq Mumtaz, Shahabuddin Muhammad, Muhammad Imran Aslam and Nazeeruddin Mohammad. Dual Connectivity-Based Mobility Management and Data Split Mechanism in 4G/5G Cellular Networks. IEEE Access, 20. 2020. [Presents techniques for handovers in mobile phone networks using probabilistic model checking and PRISM.]
[PRSG20] Ashutosh Pandey, Ivan Ruchkin, Bradley Schmerl and David Garlan. Hybrid Planning Using Learning and Model Checking for Autonomous Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20). 2020. [Presents a hybrid planning technique for autonomous systems combining learning and model checking, the latter using PRISM.]
[TLHW] Milan Tomy, Bruno Lacerda, Nick Hawes and Jeremy L Wyatt. Battery Charge Scheduling in Long-Life Autonomous Mobile Robots. Robotics and Autonomous Systems, 133. 2020. [Proposes techniques for battery charge scheduling in autonomous mobile robots, using multi-objective model checking in PRISM.]
[ZBD20] Xi Zheng, Matthew L. Bolton and ChristopherDaly. Extended SAFPH℞ (Systems Analysis for Formal Pharmaceutical Human Reliability): Two approaches based on extended CREAM and a comparative analysis. Safety Science, 132. 2020. [Presents an approach to predict error rates in pharmacies using probabilistic model checking and PRISM.]
[NKF20] Mehran Alidoost Nia, Mehdi Kargahi and Fathiyeh Faghiha. Probabilistic approximation of runtime quantitative verification in self-adaptive systems. Microprocessors and Microsystems, 72. 2020. [Proposes approximate verification techniques for self-adaptive systems, using an extension of PRISM as an underlying model checker.]
[LL20] Yang Liu and Rui Li. Compositional Stochastic Model Checking Probabilistic Automata via Assume-guarantee Reasoning. International Journal of Networked and Distributed Computing, 8(2), pages 94-107. 2020. [Proposes compositional methods for probabilistic model checking, implemented as an extension of PRISM.]
[NKA20] Mehran Alidoost Nia, Mehdi Kargahi and Alessandro Abate. Self-Adaptation with Imperfect Monitoring in Solar Energy Harvesting Systems. In Proc. CSI/CPSSI International Symposium on Real-Time and Embedded Systems and Technologies (RTEST'20). 2020. [Proposes model-driven techniques for analysing self-adaptive solar energy harvesting systems using PRISM as an underlying model checker.]
[BGJS20] Hugo Bazille, Blaise Genest, Cyrille Jegourel and Jun Sun. Global PAC Bounds for Learning Discrete Time Markov Chains. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 304-326, Springer. 2020. [Presents methods for learning Markov chains from samples, with an implementation built on PRISM's simulator.]
[SGDE20] Giorgos Stamatelatos, Sotirios Gyftopoulos, George Drosatos and Pavlos S. Efraimidis. Revealing the political affinity of online entities through their Twitter followers. Information Processing & Management, 57(2), Elsevier. 2020. [Presents methods for analysing the Twitter network, using PRISM as a Markov chain solver.]
[JZZD20] Li Jin, Guoan Zhang, Hao Zhu and Wei Duan. SDN-Based Survivability Analysis for V2I Communications. Sensors, 20. 2020. [Performs verification of networking within vehicle-to-infrastructure communications using PRISM.]
[LAKG20] Nianyu Li, Sridhar Adepu, Eunsuk Kang and David Garlan. Explanations for Human-on-the-loop: A Probabilistic Model Checking Approach. In Proc. IEEE/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'20). 2020. [Presents techniques for human-on-the-loop systems using probabilistic model checking and PRISM.]
[RB20] Kaustabha Ray and Ansuman Banerjee. Trace-driven Modeling and Verification of a Mobility-Aware Service Allocation and Migration Policy for Mobile Edge Computing. In Proc. IEEE International Conference on Web Services (ICWS'20), pages 310-317. 2020. [Uses PRISM to verify a mobility-aware service allocation policy for mobile edge computing.]
[GGP20] Debjani Ghosh, Satya Sankalp Gautam and Mayank Pandey. An Extension For PRISM Model Checker To Reduce Computation Time For Steady State Probability Analysis. In Proc. International Conference on Innovative Trends in Information Technology (ICITIIT'20). 2020. [Proposes an extension of PRISM focusing on computing steady-state probabilities.]
[GC20] Mario Gleirscher and Radu Calinescu. Safety Controller Synthesis for Collaborative Robots. In Proc. 25th International Conference on Engineering of Complex Computer Systems (ICECCS'20). 2020. [Introduces techniques and tool support for automatic safety controllers in human-robot collaboration, including use of PRISM.]
[MJIB20] Ahmad Mohsin, Naeem Khalid Janjua, Syed M. S. Islam and Muhammad Ali Babar. SAM-SoS: A Stochastic Software Architecture Modeling and Verification Approach for Complex System-of-Systems. IEEE Access, 8. 2020. [Proposes an approach for modelling and verifying System-of-Systems (SoS) based on a translation to PRISM.]
[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), volume 12479 of LNCS, pages 216-241, Springer. 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.]
[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), volume 12288 of LNCS, pages 231-248, Springer. September 2020. [pdf] [bib] [Proposes techniques for probabilistic verification of deep reinforcement learning policies, using PRISM as an underlying model checker.]
[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.]
[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.]
[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. June 2020. [pdf] [bib] [Analyses the effectiveness of certificate transparency gossiping protocols using probabilistic model checking and PRISM.]
[FGH+20] Douglas Fraser, Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin Norman. Collaborative Models for Autonomous Systems Controller Synthesis. Formal Aspects of Computing, 32, pages 157-186. April 2020. [pdf] [bib] [Synthesises controllers for unmanned aerial vehicles using probabilistic model checking and PRISM.]

2019

[Gom19] Mauricio Gonzalez Gomez. Stochastic Games on Graphs with Applications to Smart-Grids Optimization. Ph.D. thesis, French National Center for Scientific Research (CNRS), University of Paris-Saclay. 2019. [Presents formal methods for power consumption scheduling including the use of PM RISM.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[SDK+20] Muhammad Usama Sardar, Clemens Dubslaff, Sascha Klüppelholz, Christel Baier and Akash Kumar. Performance Evaluation of Thermal-Constrained Scheduling Strategies in Multi-core Systems. In Proc. European Workshop on Performance Engineering (EPEW'19), volume 12039 of LNCS, pages 133-147, Springer. 2019. [Performs formal verification of scheduling strategies for multi-core systems using PRISM.]
[DCV+19] Nicolas Dejon, Davide Caputo, Luca Verderame, Alessandro Armando and Alessio Merlo. Automated Security Analysis of IoT Software Updates. In Proc. IFIP International Conference on Information Security Theory and Practice (WISTP'19), Springer. 2019. [Presents the automated software analysis framework IoTAV, which uses PRISM as an underlying model checker.]
[MWA19] Gareth W. Molyneu, Viraj B. Wijesuriya and Alessandro Abate. Bayesian Verification of Chemical Reaction Networks. In Proc. International Symposium on Formal Methods (FM'19) Workshops, pages 461-479. 2019. [Presents a bayesian approach to verification of chemical reaction networks, using PRISM's parametric model checking functionality.]
[DKT19] Clemens Dubslaff, Patrick Koopmann and Anni-Yasmin Turhan. Ontology-Mediated Probabilistic Model Checking. In Proc. International Conference on Integrated Formal Methods (IFM'19). 2019. [Presents an ontology-mediated approach to probabilistic model checking, building upon PRISM for the implementation.]
[Vis19] Luisa Vissat. Modelling and spatio-temporal analysis of spatial stochastic systems. Ph.D. thesis, University of Edinburgh. 2019. [Introduces methods for formal analysis of spatial stochastic systems, with validation performed using PRISM.]
[BMBO19] Abdelhakim Baouya, Otmane Ait Mohamed, Djamal Bennouar and Samir Ouchani. Safety analysis of train control system based on model-driven design methodology. Computers in Industry. 2019. [Performs safety analysis of train control systems using AADL and probabilistic model checking with PRISM.]
[BXACD19] Xin Bai, Chenghao Xu, Yi Ao, Biao Chen and Dehui Du. Learning-based Probabilistic Modeling and Verifying Driver Behavior using MDP. In Proc. International Symposium on Theoretical Aspects of Software Engineering (TASE'19), pages 152-159. 2019. [Builds and analyses models of driver behaviour, using PRISM to solve MDPs.]
[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.]
[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.]
[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.]
[UNI19] Riaz Uddin, Syed Atif Naseem and Zafar Iqbal. Formal Reliability Analyses of Power Line Communication Network-based Control in Smart Grid. International Journal of Control, Automation and Systems, Springer. 2019. [Analyses the reliability of smart grid communication networks using probabilistic model checking and PRISM.]
[HAS19] Khaza Anuarul Hoque, Otmane Ait Mohamed and Yvon Savaria. Dependability Modeling and Optimization of Triple Modular Redundancy Partitioning for SRAM-based FPGAs. Reliability Engineering & System Safety. 2019. [Presents a methodology to analyse Triple Modular Redundancy (TRM) using probabilistic model checking and 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.]
[GBK+19] Safa Guellouz, Adel Benzina, Mohamed Khalgui, Georg Frey, Zhiwu Liv and Valeriy Vyatkin. Designing Efficient Reconfigurable Control Systems Using IEC61499 and Symbolic Model Checking. IEEE Transactions on Automation Science and Engineering, 16(3), pages 1110-1124. 2019. [Presents an approach for modelling and verification of reconfigurable distributed system, using PRISM as a back-end verifier. ]
[ZRF+19] Xingyu Zhao, Valentin Robu, David Flynn, Fateme Dinmohammadi, Michael Fisher and Matt Webster. Probabilistic Model Checking of Robots Deployed in Extreme Environments. In Proc. Thirty-Third AAAI Conference on Artificial Intelligence. 2019. [Proposes a probabilistic model checking approach for verifying the safety of robots in hazardous environments, based on the use of PRISM.]
[SCRVP19] Gabriela Félix Solano, Ricardo Diniz Caldas, Genaína Nunes Rodrigues, Thomas Vogel and Patrizio Pelliccione. Taming Uncertainty in the Assurance Process of Self-Adaptive Systems: a Goal-Oriented Approach. In Proc. 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'19). 2019. [Proposes an assurance process for self-adaptive systems, with an implementation based on PRISM.]
[CS19] Muffy Calder and Michele Sevegnani. Stochastic model checking for predicting component failures and service availability. IEEE Transactions on Dependable and Secure Computing, 16(1), pages 174-187. 2019. [Uses probabilistic model checking and PRISM for a formal analysis to support the management of a critical communications service.]
[SKK+19] Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen and Alexandra Silva. Scalable Verification of Probabilistic Networks. In Proc. 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19), pages 190-203. 2019. [Presents a tool, McNetKAT, for verifying probabilistic network programs, optionally using PRISM as a backend solver.]
[ELK19] Francisco Eiras, Morteza Lahijanian and Marta Kwiatkowska. Correct-by-Construction Advanced Driver Assistance Systems Based on a Cognitive Architecture. In Proc. IEEE 2nd Connected and Automated Vehicles Symposium (CAVS'19), pages 1-7, IEEE. 2019. [pdf] [bib] [Formally analyses a driver assistance system and a human driver model, with an implementation building on PRISM.]
[WDSX19] Xiaomin Wei, Yunwei Dong, Pengpeng Sun and Mingrui Xiao. Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games. Electronics, 8(2). 2019. [Formally analyses grid cyber-physical systems using PRISM-games.]
[AT19] Bernhard K. Aichernig and Martin Tappler. Probabilistic black-box reachability checking. Formal Methods in System Design, 54, pages 416–448. 2019. [Presents a black-box checking technique for probabilistic systems, including the use of PRISM.]
[MP19] P. Milazzo and G. Pardini. Objective/MC: A high-level model checking language. Journal of Intelligent Information Systems volume, 52, pages 533–571. 2019. [Presents a high-level imperative modelling language and a translation into PRISM.]
[PMT19] Lorenzo Pagliari, Raffaela Mirandola and Catia Trubiani. Engineering cyber-physical systems through performance-based modelling and analysis: A case study experience report. Journal of Software: Evolution and Process, 32(1). 2019. [Presents a model-based analysis of a delivery robots system, including the use of probabilistic model checking and PRISM.]
[PTM19] Bernd Porr, Alex Trew and Alice Miller. An investigation into serotonergic and environmental interventions against depression in a simulated delayed reward paradigm. Adaptive Behavior. 2019. [Studies serotonergic and environmental interventions against depression using both simulation an probabilistic model checking, the latter using PRISM.]
[ZOL+19] Xingyu Zhao, Matthew Osborne, Jennifer Lantair, Valentin Robu, David Flynn, Xiaowei Huang, Michael Fisher, Fabio Papacchini and Angelo Ferrando. Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. In Proc. 17th International Conference on Software Engineering and Formal Methods (SEFM'19), pages 105-124. 2019. [Models an unmanned aerial vehicle inspection mission on a wind farm, focusing on the battery behaviour, and using PRISM.]
[KCMS19] Ashalatha Kunnappiilly, Simin Cai, Raluca Marinescu and Cristina Seceleanu. Architecture Modelling and Formal Analysis of Intelligent Multi-Agent Systems. In Proc. 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE'19), pages 114-126. 2019. [Models and analyses a distributed ambient assisted living system represented in AADL using PRISM.]
[ZH19] Hein Htoo Zaw and Swe Zin Hlaing. Verifying the Gaming Strategy of Self-learning Game by Using PRISM-Games. In Proc. International Conference on Intelligent Computing & Optimization (ICO'19), volume 1072 of AISC, pages 148-159. 2019. [Studies learning based approaches for MDP policy synthesis, using PRISM-games as a model checker.]
[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.]
[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.]
[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.]
[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.]
[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

[JJK+18] Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang and Mary Hayhoe. Model Checking for Safe Navigation Among Humans. In Proc. 15th International Conference on Quantitative Evaluation of SysTems (QEST'18), volume 11024 of LNCS, pages 207-222, Springer. 2018. [bib] [Applies probabilistic model checking to autonomous system operating alongside uncontrollable agents such as humans, including use of PRISM-games for stochastic game models.]
[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.]
[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.]
[NEU18] Syed Atif Naseem, Raheleh Eslampanah and Riaz Uddin. Probability estimation for the fault detection and isolation of pmu-based transmission line system of smart grid. In Proc. 2018 5th International Conference on Electrical and Electronic Engineering (ICEEE). 2018. [Proposes methods for fault detection and isolation in smart grids via an analysis in PRISM.]
[PBM18] Sophia Petridou, Stylianos Basagiannis and Lefteris Mamatas. Formal Methods for Energy-Efficient EPONs. IEEE Transactions on Green Communications and Networking, 2(1), pages 246-259. 2018. [Performs formal modelling and analysis of Ethernet Passive Optical Networks (EPONs) using PRISM.]
[LCHL18] Zipeng Li, Krishnendu Chakrabarty, Tsung-Yi Ho and Chen-Yi Lee. Efficient and Adaptive Error Recovery. In Micro-Electrode-Dot-Array Digital Microfluidic Biochips, pages 53-81, Springer. 2018. [Presents local recovery strategies for biochips, evaluated using PRISM.]
[Guo18] Xu Guo. Performance analysis of Israeli-Jalfon's algorithm using probabilistic model checking. Concurrency and Computation: Practice and Experience. 2018. [Uses probabilistic model checking and PRISM to verify Israeli‐Jalfon's self‐stabilization algorithm.]
[CPGS18] Javier Cámara, Wenxin Peng, David Garlan and Bradley Schmerl. Reasoning about sensing uncertainty and its reduction in decision-making for self-adaptation. Science of Computer Programming, 167, pages 51-69, Elsevier. 2018. [Proposes a formal analysis technique for self-adaptive decision making under sensor uncertainty, building on the PRISM-games framework.]
[MGK18] Maria Maximova, Holger Giese and Christian Krause. Probabilistic timed graph transformation systems. Journal of Logical and Algebraic Methods in Programming. 2018. [Presents the Probabilistic Timed Graph Transformation Systems formalism, with a mapping to PRISM. ]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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. [bib] [Proposes a framework for analysing resource-performance trade-offs in mobile robotics, using PRISM as an underlying model checker.]
[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.]
[Ouc18] Samir Ouchani. Ensuring the Functional Correctness of IoT through Formal Modeling and Verification. In Proc. International Conference on Model and Data Engineering (MEDI'18), pages 401-417. 2018. [Verifies the functionality and security of IoT systems using PRISM.]
[NUHF18] Syed Atif Naseem, Riaz Uddin, Osman Hasan and Diaa E. Fawzy. Probabilistic Formal Verification of Communication Network-based Fault Detection, Isolation and Service Restoration System in Smart Grid. Journal of Applied Logics. 2018. [Analyses the reliability of smart grid communication networks using probabilistic model checking and PRISM.]
[ABC+18] Alessandro Abate, Carlos Budde, Nathalie Cauchi, Khaza Anuarul Hoque and Mariëlle Stoelinga. Assessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees. In Proc. 4th European Conference of the Prognostics and Health Management Society (PHME'18). 2018. [Formally analyses maintenance policies for smart buildings using a variety of verification tools, including PRISM.]
[SAHH18] Muhammad Usama Sardar, Nida Afaq and Khaza Anuarul Hoque. Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA). Journal of Automated Reasoning. 2018. [Performs verification of NASA's Small Aircraft Transportation System (SATS) using PRISM.]
[Mas18] George Mason. Safe Reinforcement Learning Using Formally Verified Abstract Policies. Ph.D. thesis, University of York. 2018. [Proposes a reinforcement learning approach based on formally verified abstract policies, using PRISM as part of the tool chain.]
[Pat18] Colin Paterson. Observation-enhanced verification of operational processes. Ph.D. thesis, University of York. 2018. [Presents techniques for integrating observation data into probabilistic model checking, including a tool chain that uses PRISM.]
[CBGS18] M. Camilli, C. Bellettini, A. Gargantini and P. Scandurra. Online Model-Based Testing under Uncertainty. In Proc. IEEE 29th International Symposium on Software Reliability Engineering (ISSRE'18), pages 36-46. 2018. [Proposes a model-based testing technique using uncertainty-aware sampling, and deploying PRISM for the analysis of MDPs.]
[DMJ18] Kai Ding, Andrey Morozov and Klaus Janschek. Reliability Evaluation of Functionally Equivalent Simulink Implementations of a PID Controller under Silent Data Corruption. In Proc. IEEE 29th International Symposium on Software Reliability Engineering (ISSRE'18), pages 47-57. 2018. [Proposes a method for formal system reliability evaluation, based on the tool OpenErrorPro and using PRISM as a backend.]
[GWH18] Min Gao, Kun Wang and Lei He. Probabilistic Model Checking and Scheduling Implementation of an Energy Router System in Energy Internet for Green Cities. Proc. IEEE Transactions on Industrial Informatics, 14(4), pages 1501-1510. 2018. [Formally verifies an energy router based system using probabilistic model checking and PRISM. ]
[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.]
[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.]
[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.]
[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.]
[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.]
[GHI+18] Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller and Gethin Norman. Strategy Synthesis for Autonomous Agents using PRISM. In Proc. 10th NASA Formal Methods Symposium (NFM 2018), volume 10811 of LNCS, pages 220-236, Springer. March 2018. [pdf] [bib] [Synthesises controllers for unmanned aerial vehicles using probabilistic model checking and 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

[GCSW17] Simos Gerasimou, Radu Calinescu, Stepan Shevtsov and Danny Weyns. UNDERSEA: An Exemplar for Engineering Self-Adaptive Unmanned Underwater Vehicles. In Proc. 2017 IEEE/ACM 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'17), pages 83-89. 2017. [Presents a self-adaptive UUV case study, incorporating runtime probabilistic model checking with 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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[IK17] Azlan Ismail and Marta Kwiatkowska. Synthesizing Pareto Optimal Decision for Autonomic Clouds using Stochastic Games Model Checking. In Proc. 24th Asia-Pacific Software Engineering Conference (APSEC'17), pages 436-445, IEEE. 2017. [pdf] [bib] [Proposes a multi-objective adaptive decision-making approach for autonomic clouds based on PRISM-games.]
[SSHHA17] Adnan Yaqoob Salik, Muhammad Usama Sardar, Osman Hasan, Syed Rafay Hasan and Falah Awwad. Formal verification of demand response based home energy management systems in smart grids. In Proc. IEEE Innovative Smart Grid Technologies - Asia (ISGT Asia). 2017. [Presents a formal analysis of a smart grid demand response management system using PRISM.]
[RDR+17] Yasmin Rafiq, Luke Dickens, Alessandra Russo, Arosha Bandara, Mu Yang, Avelie Stuart, Mark Levine, Gul Calikli, Blaine Price and Bashar Nuseibeh. Learning to Share: Engineering Adaptive Decision-Support for Online Social Networks. In Proc. 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE'17). 2017. [Proposes an adaptive privacy control approach for social networks, including modelling and analysis of the approach using PRISM.]
[BKW17] Nicolas Basset, Marta Kwiatkowska and Clemens Wiltsche. Compositional Strategy Synthesis for Stochastic Games with Multiple Objectives. Information and Computation, 261(3), pages 536-587. 2017. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, along with a compositional assume-guarantee strategy synthesis framework.]
[MGK17] Maria Maximova, Holger Giese and Christian Krause. Probabilistic Timed Graph Transformation Systems. In Proc. International Conference on Graph Transformation (ICGT'17). 2017. [Presents the Probabilistic Timed Graph Transformation Systems formalism, with a mapping to 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.]
[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.]
[BMM17] Sania Bhatti, Mohsin Memon, and Sheeraz Memon. Evaluating FTTT Protocol via PRISM, PRISM-symm and GRIP. International Journal of Computer Theory and Engineering, 9(3), pages 162-166. 2017. [Performs probabilistic model checking of the of Fault Tolerant Target Tracking (FTTT) protocol using PRISM and related tools.]
[MCKB17] George Mason, Radu Calinescu, Daniel Kudenko and Alec Banks. Assured Reinforcement Learning with Formally Verified Abstract Policies. In Proc. 9th International Conference on Agents and Artificial Intelligence (ICAART'17). 2017. [Proposes a reinforcement learning approach based on formally verified abstract policies, using PRISM as part of the tool chain.]
[CCGKP17] Radu Calinescu, Milan Češka, Simos Gerasimou, Marta Kwiatkowska and Nicola Paoletti. Designing Robust Software Systems through Parametric Markov Chain Synthesis. In Proc. IEEE International Conference on Software Architecture (ICSA'17), pages 131-140, IEEE Computer Society. 2017. [pdf] [bib] [Synthesises software system designs with a toolchain building on the PRISM extension PRISM-PSY.]
[ACDKM17] Pranav Ashok, Krishnendu Chatterjee, Przemysław Daca, Jan Křetínský and Tobias Meggendorfer. Value Iteration for Long-run Average Reward in Markov Decision Processes. In Proc. International Conference on Computer Aided Verification (CAV'17), pages 201-221. 2017. [Implements a novel algorithm for solving long-run average MDPs as an extension of PRISM.]
[PBM17] Sophia Petridou, Stylianos Basagiannis and Lefteris Mamatas. Energy-efficiency analysis under QoS constraints using formal methods: A study on EPONs. In Proc. IEEE International Conference on Communications (ICC'17), pages 1-6. 2017. [Performs formal modelling and analysis of Ethernet Passive Optical Networks (EPONs) using PRISM.]
[BRS17] Zeeshan E. Bhatti, Partha S. Roop and Roopak Sinha. Unified Functional Safety Assessment of Industrial Automation Systems. IEEE Transactions on Industrial Informatics, 13(1), pages 17-26. 2017. [Uses probabilistic model checking and PRISM to analyse IEC 61499 designs for industrial automation systems.]
[Kap17] Tatjana Kapus. Using PRISM model checker as a validation tool for an analytical model of IEEE 802.15.4 networks. Simulation Modelling Practice and Theory, 77, pages 367-378. 2017. [Considers the analysis of IEEE 802.15.4 networks using probabilistic model checking and PRISM.]
[MMBK17] Nazeeruddin Mohammad, Shahabuddin Muhammad, Abul Bashar and Majid Ali Khan. Design and modeling of energy efficient WSN architecture for tactical applications. In Proc. Military Communications and Information Systems Conference (MilCIS'17), pages 1-6. 2017. [Proposes a wireless sensor network architecture and verifies it using PRISM.]
[AT17] Bernhard K. Aichernig and Martin Tappler. Probabilistic black-box reachability checking. In Proc. 17th International Conference on Runtime Verification (RV'17). 2017. [Presents a black-box checking technique for probabilistic systems, including the use of PRISM.]
[Spr17] Jeremy Sproston. Probabilistic Timed Automata with Clock-Dependent Probabilities. In Proc. 11th International Workshop on Reachability Problems (RP'17), Springer. 2017. [Develops techniques for PTAs in which transition probabilities can depend on clocks, including experiments performed using PRISM.]
[KKS17] Maria Krotsiani, Christos Kloukinas and George Spanoudakis. Cloud Certification Process Validation using Formal Methods. In Proc. International Conference on Service-Oriented Computing (ICSOC'17), pages 65-79. 2017. [Proposes an approach for formal certification of cloud systems using a translation to PRISM.]
[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.]
[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.]
[LPH17] Bruno Lacerda, David Parker and Nick Hawes. Multi-objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees. In Proc. 27th International Conference on Automated Planning and Scheduling (ICAPS'17), pages 504-512, AAAI Press. June 2017. [pdf] [bib] [Proposes techniques for generating mobile robot controllers with probabilistic time-bounded guarantees using multi-objective probabilistic model checking and an extension of PRISM.]
[EPB17] Alexandros Evangelidis, David Parker and Rami Bahsoon. Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. In Proc. IEEE/ACM 17th International Symposium on Cluster, Cloud and Grid Computing (CCGrid'17), pages 355-364, IEEE. May 2017. [pdf] [bib] [Presents an approach for producing formal performance guarantees for cloud-based auto-scaling policies using PRISM.]
[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

[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.]
[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.]
[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.]
[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.]
[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. [bib] [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements. ]
[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.]
[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.]
[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.]
[SSB+16] Dongwon Seo, Donghwan Shin, Young-Min Baek, Jiyoung Song, Wonkyung Yun, Junho Kim, Eunkyoung Jee and Doo-Hwan Bae. Modeling and Verification for Different Types of System of Systems using PRISM. In Proc. IEEE/ACM 4th International Workshop on Software Engineering for Systems-of-Systems (SESoS'16), pages 12-18. 2016. [Proposes a modelling scheme for system of systems (SoS) and uses PRISM for verification.]
[Mun16] Peter Munk. A Software Fault-Tolerance Mechanism for Mixed-Critical Real-Time Applications on Consumer-Grade Many-Core Processors. Ph.D. thesis, University of Berlin. 2016. [Presents an adaptive fault-tolerance mechanism for many-core processors including a model analysis using PRISM.]
[MHGSH16] Awais Mahmood, Osman Hasan, Hassan Raza Gillani, Yassar Saleem and Syed Rafay Hasan. Formal reliability analysis of protective systems in smart grids. In Proc. 2016 IEEE Region 10 Symposium (TENSYMP). 2016. [Provides a reliability assessment of smart grids using PRISM.]
[FCB+16] João M. Franco, Francisco Correia, Raul Barbosa, Mário Zenha-Rela, Bradley Schmerl and David Garlan. Improving self-adaptation planning through software architecture-based stochastic modeling. Journal of Systems and Software, 115, pages 42-60. 2016. [Proposes a stochastic modelling approach for self-adaptive software with analysis performed using PRISM. ]
[SRT16] Guoxin Su, David S. Rosenblum and Giordano Tamburrelli. Reliability of Run-Time Quality-of-Service Evaluation Using Parametric Model Checking. In Proc. IEEE/ACM 38th International Conference on Software Engineering (ICSE'16), pages 73-84. 2016. [Presents techniques for assessing quality of service using parametric probabilistic model checking, and a tool chain involving PRISM.]
[HIM+16] Ruth Hoffmann, Murray L. Ireland, Alice Miller, Gethin Norman and Sandor M. Veres. Autonomous Agent Behaviour Modelled in PRISM - A Case Study. In Proc. 23rd International Symposium on Model Checking Software (SPIN'16), pages 104-110. 2016. [Describes the modelling and verification of an unmanned aerial vehicle (UAV) using PRISM.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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. ]
[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.]
[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.]
[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.]
[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. ]
[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.]
[LZW+16] Lulu Liang, Kai Zheng, Zilong Wei, Yanmei Wang, Sihan Wu and Xin Huang. Model Checking of IoT System in Microgrid. In Proc. IEEE International Symposium on Information in Medicine and Education (ITME'16). 2016. [Verifies the reliability of IoT systems in microgrids using probabilistic model checking and PRISM.]
[CJP16] Radu Calinescu, Kenneth Johnson and Colin Paterson. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. In Proc. TACAS'16, volume 9636 of LNCS, pages 540-546, Springer. 2016. [Presents a model checker for computing confidence intervals, building on PRISM's parametric model checking functionality.]
[PMCG16] Ashutosh Pandey, Gabriel A. Moreno, Javier Cámara and David Garlan. Hybrid Planning for Decision Making in Self-Adaptive Systems. In Proc. 10th International Conference on Self-Adaptive and Self-Organizing Systems (SASO'16). 2016. [Presents a hybrid planning technique for self-adaptive systems combining learning and probabilistic model checking, with an implementation based on PRISM.]
[GBKF16] Safa Guellouz, Adel Benzina, Mohamed Khalgui, Georg Frey. ZiZo: A Complete Tool Chain for the Modeling and Verification of Reconfigurable Function Blocks. In Proc. 10th International Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies (UBICOMM'16). 2016. [Presents a tool-chain for modelling and verification of reconfigurable distributed system, using PRISM as a back-end verifier.]
[FWHT16] Lu Feng, Clemens Wiltsche, Laura Humphrey and Ufuk Topcu. Synthesis of Human-in-the-Loop Control Protocols for Autonomous Systems. IEEE Transactions on Automation Science and Engineering, 13(2), pages 450-462. 2016. [bib] [Uses PRISM and PRISM-games to synthesize control protocols for autonomous systems interacting with human operators.]
[KRF16] Lubos Korenciak, Vojtech Rehak and Adrian Farmadin. Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC. In Proc. 12th International Conference on Integrated Formal Methods (IFM'16), volume 9681 of LNCS, pages 130-138, Springer. 2016. [Presents an extension of PRISM to support fixed-delay continuous-time Markov chains (fdCTMCs).]
[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.]
[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.]
[ANP16] Zaruhi Aslanyan, Flemming Nielson and David Parker. Quantitative Verification and Synthesis of Attack-Defence Scenarios. In Proc. 29th IEEE Computer Security Foundations Symposium (CSF'16), pages 105-119, IEEE. June 2016. [pdf] [bib] [Proposes formal verification techniques for attack-defence scenarios based on model checking of stochastic games and building on the PRISM-games tool.]
[KPW16] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), volume 9636 of LNCS, pages 560-566, Springer. April 2016. [pdf] [bib] [Introduces version 2.0 of the PRISM-games tool.]
[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. ]
[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

[RA15] Misbah Razzaq,Jamil Ahmad. Petri Net and Probabilistic Model Checking Based Approach for the Modelling, Simulation and Verification of Internet Worm Propagation. PLOS ONE. 2015. [Presents an approach based on stochastic Petri nets and PRISM for analysing internet worms.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[SNR15] M. Shafiuzzaman, N. Nahar and M. R. Rahman. A proactive approach for context-aware self-adaptive mobile applications to ensure Quality of Service. In Pro. 18th International Conference on Computer and Information Technology (ICCIT'15), pages 544-549. 2015. [Proposes an approach for analysing quality of service in mobile applications using probabilistic model checking and PRISM.]
[IHSH15] Shafaq Iqtedar, Osman Hasan, Muhammad Shafique and Jörg Henkel. Probabilistic Formal Verification Methodology for Decentralized Thermal Management in On-Chip Systems. In Proc. IEEE 24th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises. 2015. [Analyses dynamic thermal management schemes for multi-core architectures using PRISM.]
[BBMO15] Abdelhakim Baouya, Djamal Bennouar, Otmane Ait Mohamed and Samir Ouchani. A quantitative verification framework of SysML activity diagrams under time constraints. Expert Systems with Applications. 2015. [Proposes a verification framework using the SysML formalism and probabilistic model checking with PRISM.]
[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.]
[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.]
[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.]
[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.]
[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. [bib] [Proposes techniques for architecture-based self-adapation using stochastic multi-player games and PRISM-games.]
[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.]
[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.]
[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.]
[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.]
[NSKG15] Athanasios Naskos, Emmanouela Stachtiari, Panagiotis Katsaros and Anastasios Gounaris. Probabilistic model checking at runtime for the provisioning of cloud resources. In Proc. 6th International Conference on Runtime Verification (RV'15). 2015. [Presents a model-driven approach for the dynamic cloud provisioning 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.]
[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.]
[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.]
[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.]
[HMS15b] Ghaith Bany Hamad, Otmane Ait Mohamed, and Yvon Savaria. Efficient multilevel formal analysis and estimation of design vulnerability to Single Event Transients. In Proc. 21st IEEE International On-Line Testing Symposium (IOLTS'15), pages 1-6. 2015. [Develops a methodology to investigate the impact of Single Event Transients (SETs) on digital design reliability using PRISM.]
[MTJ15] Andrey Morozov, Regina Tuk, Klaus Janschek. ErrorPro: Software Tool for Stochastic Error Propagation Analysis. In 1st International Workshop on Resiliency in Embedded Electronic Systems, Amsterdam, The Netherlands. 2015. [Presents a tool for stochastic error propagation analysis using PRISM as a backend solver.]
[IHSK15] Shafaq Iqtedar, Osman Hasan, Muhammad Shafique and Jörg Henkel. Formal probabilistic analysis of distributed dynamic thermal management. In Proc. Design, Automation & Test in Europe Conference & Exhibition (DATE'15), pages 1221-1224. 2015. [Verifies a distributed scheme for dynamic thermal management using PRISM. ]
[BBGKS15] Sinem Getir, Lars Grunske, Christian Karl Bernasko, Verena Kafer and Tim Sanwald. CoWolf - A Generic Framework for Multi-View Co-Evolution and Evaluation of Models. In Proc. Intl. Conference on Theory and Practice of Model Transformations (ICMT'15), pages 34-40. 2015. [Presents a framework and tool environment for modelling with support for co-evolution, including PRISM as a backend solver.]
[LOP+15] Michael Lipaczewski, Frank Ortmeier, Tatiana Prosvirnova, Antoine Rauzy and Simon Struck. Comparison of modeling formalisms for Safety Analyses: SAML and AltaRica. Reliability Engineering & System Safety, 140, pages 191-199. 2015. [Compares formalisms for safety analyses, with various underlying tools, including PRISM.]
[NPZ15] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Real-Time Systems. In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of LNCS, pages 240-255, Springer. September 2015. [pdf] [bib] [Develops techniques for verification and controller synthesis on a partially observable variant of probabilistic timed automata, implemented in an extension of PRISM.]
[LPH15] Bruno Lacerda, David Parker and Nick Hawes. Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications. In Proc. 24th International Joint Conference on Artificial Intelligence (IJCAI'15), pages 1587-1593, IJCAI/AAAI. August 2015. [pdf] [bib] [Proposes techniques for synthesising optimal policies in MDPs, building on multi-objective probabilistic model checking and PRISM, and applies them to robot task planning.]
[BBDL+15] Tomas Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretinsky, David Muller, David Parker and Jan Strejcek. The Hanoi Omega-Automata Format. In Proc. 27th International Conference on Computer Aided Verification (CAV'15), volume 9206 of LNCS, pages 479-486, Springer. July 2015. [pdf] [bib] [Proposes an exchange format for omega automata, and describes implemented support in a variety of tools, including PRISM.]
[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

[SLBK14] Richard Skowyra, Andrei Lapets, Azer Bestavros and Assaf Kfoury. A Verification Platform for SDN-Enabled Applications. In Proc. 2014 IEEE International Conference on Cloud Engineering. 2014. [Presents a verification platform for software defined networks with multiple tool connections, including PRISM.]
[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.]
[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]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[GCB14] Simos Gerasimou, Radu Calinescu and Alec Banks. Efficient Runtime Quantitative Verification using Caching, Lookahead, and Nearly-Optimal Reconfiguration. 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.]
[JKSH14] Ali Jafari, Ehsan Khamespanah, Marjan Sirjani and Holger Hermanns. Performance Analysis of Distributed and Asynchronous Systems using Probabilistic Timed Actors. In Proc. 14th International Workshop on Automated Verification of Critical Systems (AVoCS'14). 2014. [Proposes an actor-based language for probabilistic timed systems, connecting to PRISM for probabilistic model checking.]
[CLGS14] Javier Cámara, Antónia Lopes, David Garlan and Bradley Schmerl. Impact Models for Architecture-Based Self-adaptive Systems. In Proc. International Conference on Formal Aspects of Component Software (FACS'14), pages 89-107, Springer. 2014. [Proposes techniques based on probabilistic impact model for self-adaptive systems, using PRISM an underlying solver.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[CR14] Gabriel Ciobanu and Armand Stefan Rotaru. PHASE: A Stochastic Formalism for Phase-Type Distributions. In Proc. International Conference on Formal Engineering Methods (ICFEM'14), pages 91-106. 2014. [Presents a stochastic process calculus for non-Markovian systems and a translation to PRISM.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[BCC+14] Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelík, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, David Parker and Mateusz Ujma. Verification of Markov Decision Processes using Learning Algorithms. In Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA'14), volume 8837 of LNCS, pages 98-114, Springer. November 2014. [pdf] [bib] [Presents MDP verification techniques, implemented in PRISM, based on real-time dynamic programming and delayed Q-learning.]
[LPH14b] Bruno Lacerda, David Parker and Nick Hawes. Optimal and Dynamic Planning for Markov Decision Processes with Co-Safe LTL Specifications. In Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'14), pages 1511-1516, IEEE. September 2014. [pdf] [bib] [Proposes a dynamic planning approach for co-safe LTL, implements it in an extension of PRISM and deploys it on a mobile service robot.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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

[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.]
[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. ]
[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.]
[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.]
[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.
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[BCFCC13] Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos and Sérgio V. A. Campos. Probabilistic Model Checking Analysis of Palytoxin Effects on Cell Energy Reactions of the Na+/K+-ATPase. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 10(6), pages 1530-1541. 2013. [Analyses palytoxin toxin interactions within cell transport systems using probabilistic model checking and PRISM.]
[PBU13] Esteban Pavese, Víctor Braberman and Sebastián Uchitel. Automated reliability estimation over partial systematic explorations. In Proc. 35th International Conference on Software Engineering (ICSE'13). 2013. [Presents a method for formal reliability estimation using simulation, invariant inference and probabilistic model checking, and building upon PRISM.]
[CGMS13] Javier Camara, David Garlan, Gabriel Moreno and Bradley Schmerl. Analyzing Self-adaptation Via Model Checking of Stochastic Games. In Software Engineering for Self-Adaptive Systems, Springer. 2013. [Describes an approach for the analysis of self-adaptive systems using PRISM-games.]
[SM13] Amir Molzam Sharifloo and Andreas Metzger. MCaaS: Model Checking in the Cloud for Assurances of Adaptive Systems. In Software Engineering for Self-Adaptive Systems, Springer. 2013. [Describes a cloud-based approach to the assurance of adaptive systems with an evaluation that uses PRISM for probabilistic model checking tasks.]
[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.]
[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.]
[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.]
[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.]
[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. ]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[CFK+13] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of LNCS, pages 185-191, Springer. March 2013. [pdf] [bib] [Introduces PRISM-games, a model checker for stochastic multi-player games.]
[KPS13] Marta Kwiatkowska, David Parker and Aistis Simaitis. Strategic Analysis of Trust Models for User-Centric Networks. In Proc. 1st International Workshop on Strategic Reasoning (SR'13), volume 112 of EPTCS, pages 53-60. March 2013. [pdf] [bib] [Analyses a cooperation model for user-centric networks using PRISM-games.]
[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.]
[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

[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).]
[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.]
[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.]
[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.]
[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.]
[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. [bib] [Applies PRISM to the analysis of probabilistic Boolean networks, using an apoptosis network and a WNT5A network as examples.]
[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.
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[WBM12] Matthias Woehrle, Rena Bakhshi and Mohammad Reza Mousavi. Mechanized extraction of topology anti-patterns in wireless networks. In Proc. 9th International Conference on Integrated Formal Methods (IFM'12), volume 7321 of LNCS, Springer. 2012. [Presents techniques for verifying wireless networks, including the Trickle and LMAC protocols, making use of PRISM.]
[Kum12] Jayanand Asok Kumar. Statistical Guarantees of Performance for RTL Designs. Ph.D. thesis, University of Illinois at Urbana-Champaign. 2012. [bib]
[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.]
[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.
[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.]
[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.
[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.
[OGLS12] Frank Ortmeier, Matthias Gudemann, Michael Lipaczewski and Simon Struck. Unifying Probabilistic and Traditional Formal Model Based Analysis. In Proc. MBEES. 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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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

[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]
[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]
[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]
[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]
[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
[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.
[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.
[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.
[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
[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.
[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.
[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.
[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.]
[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.]
[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]
[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]
[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]
[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]
[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]
[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]
[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]
[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]
[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]
[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]
[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]
[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.]
[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.]
[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.]
[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.]
[KNP11] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of LNCS, pages 585-591, Springer. July 2011. [pdf] [bib] [Tool paper describing PRISM 4.0.]
[KPQ11] Marta Kwiatkowska, David Parker and Hongyang Qu. Incremental Quantitative Verification for Markov Decision Processes. In Proc. IEEE/IFIP International Conference on Dependable Systems and Networks (DSN-PDS'11), pages 359-370, IEEE CS Press. June 2011. [pdf] [bib] [Presents incremental verification techniques for MDPs, implemented as an extension of PRISM.]
[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.]
[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.]
[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.]
[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.]
[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

[GO10] Matthias Gudemann and Frank Ortmeier. Probabilistic Model-Based Safety Analysis. In Proc. Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010). 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]
[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]
[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]
[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.
[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.
[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.]
[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/
[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]
[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]
[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]
[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]
[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
[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]
[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.]
[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.]
[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.]
[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.]
[FKP10] Lu Feng, Marta Kwiatkowska and David Parker. Compositional Verification of Probabilistic Systems using Learning. In Proc. 7th International Conference on Quantitative Evaluation of Systems (QEST'10), pages 133-142, IEEE CS Press. September 2010. [pdf] [bib] [Presents a learning-based compositional verification framework, based on an extension of PRISM.]
[KNP10b] Marta Kwiatkowska, Gethin Norman and David Parker. A Framework for Verification of Software with Time and Probabilities. In Proc. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of LNCS, pages 25-45, Springer. September 2010. [pdf] [bib] [Extends PRISM's game-based abstraction-refinement methods for PTAs, to real-time probabilistic programs with data.]
[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.]
[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

[HHZ09] E. Hahn, H. Hermanns and L. Zhang. Probabilistic Reachability for Parametric Markov Models. In C. Pasareanu (editor), Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 88-106, Springer. 2009. [bib]
[BKPA09] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. Probabilistic model checking for the quantification of DoS security threats. Computers & Security, Elsevier. 2009. [bib]
[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]
[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]
[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]
[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]
[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]
[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.
[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.]
[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.]
[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]
[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]
[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]
[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]
[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]
[KNP09c] Marta Kwiatkowska, Gethin Norman and David Parker. Stochastic Games for Verification of Probabilistic Timed Automata. In Proc. 7th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'09), volume 5813 of LNCS, pages 212-227, Springer. September 2009. [pdf] [bib] [Presents game-based abstraction-refinement techniques for verifying PTAs, implemented in PRISM.]
[DMP09] Alastair Donaldson, Alice Miller and David Parker. Language-level Symmetry Reduction for Probabilistic Model Checking. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), pages 289-298, IEEE Computer Society. September 2009. [pdf] [bib] [Presents symmetry reduction techniques based on translation of PRISM models.]
[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]
[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.]
[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.]
[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).]
[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.]
[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.]
[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
[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.]
[BG+09] M. ter Beek, S. Gnesi, D. Latella, M. Massink, M. Sebastianis and G. Trentanni. Assisting the Design of a Groupware System - Model Checking Usability Aspects of thinkteam. Journal of Logic and Algebraic Programming, 78(4), pages 191-232, Elsevier. April 2009. [bib]
[CK09b] R. Calinescu and M. Kwiatkowska. CADS*: Computer-Aided Development of Self-* Systems. In Marsha Chechik and Martin Wirsing (editors), Fundamental Approaches to Software Engineering (FASE 2009), volume 5503 of Lecture Notes in Computer Science, pages 421-424, Springer-Verlag. March 2009. [pdf] [bib] [Presents a tool for developing self-* systems, based on Markov chain analysis using PRISM.]
[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.]
[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.]
[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.]
[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

[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]
[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]
[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
[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]
[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
[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]
[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
[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]
[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.]
[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.]
[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
[RPNdA08] Pritam Roy, David Parker, Gethin Norman and Luca de Alfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST'08), pages 103-112, IEEE CS Press. September 2008. [pdf] [bib] [Presents a symbolic version of magnifying lens abstraction, implemented as an extension of PRISM.]
[CBGP08] Frank Ciesinski, Christel Baier, Marcus Groesser and David Parker. Generating Compact MTBDD-Representations from Probmela Specifications. In Proc. 15th International SPIN Workshop on Model Checking of Software (SPIN'08), volume 5156 of Lecture Notes in Computer Science, pages 60-76, Springer. August 2008. [pdf] [bib] [Presents techniques for efficient translation of Probmela models into the PRISM modelling language.]
[KKNP08a] Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. Game-Based Probabilistic Predicate Abstraction in PRISM. In Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08), volume 220 (3) of Electronic Notes in Theoretical Computer Science , pages 5-21 , Elsevier. March 2008. [ps.gz] [pdf] [bib] [Develops predicate abstraction techniques for PRISM, using SMT and game-based abstraction.]
[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.]
[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.]
[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.]
[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

[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/
[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]
[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]
[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
[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]
[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
[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/
[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]
[MM07] A. McIver and C. Morgan. Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic, 8(1). 2007. [bib]
[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.
[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/
[NPPW07] Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking the Probabilistic Pi-calculus. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 169-178, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents model checking techniques for the probabilistic pi-calculus based on a translation to PRISM.]
[DMP07] Alastair Donaldson, Alice Miller and David Parker. GRIP: Generic Representatives in PRISM. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 115-116, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents GRIP, a symmetry reduction tool for PRISM models.]
[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]
[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]
[LJ07] C. Langmead and S. Jha. Predicting Protein Folding Kinetics Via Temporal Logic Model Checking. In 7th International Workshop on Algorithms in Bioinformatics (WABI'07), volume 4645 of Lecture Notes in Computer Science, pages 252-264, Springer. September 2007. [bib]
[Kwi07] M. Kwiatkowska. Quantitative Verification: Models, Techniques and Tools. In Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 449-458, ACM Press. September 2007. [pdf] [bib] [Overview of probabilistic model checking and PRISM, with a particular emphasis on DTMCs.]
[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]
[KNSW07] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007. [ps.gz] [pdf] [bib]
[Vys07] V. Vyshemirsky. Probabilistic Reasoning and Inference for Systems Biology. Ph.D. thesis, University of Glasgow. July 2007. [bib] 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
[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.]
[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]
[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
[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

[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/
[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/
[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
[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.]
[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
[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]
[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.]
[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]
[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.
[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]
[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.]
[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
[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
[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]
[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
[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]
[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
[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
[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
[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.]
[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/
[KNP06e] M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. Computers & Mathematics with Applications, 51(2), pages 305-316, Elsevier. January 2006. [ps.gz] [pdf] [bib]

2005

[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.]
[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
[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]
[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/
[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]
[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
[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.]
[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/
[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/
[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/
[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/
[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
[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]
[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]
[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]
[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
[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
[Hin05] A. Hinton. Software Project M60: Simulator for the Probabilistic Model Checker PRISM. MEng Final Year Project Dissertation, School of Computer Science, University of Birmingham. April 2005. [ps.gz] [pdf] [bib]
[KNP05b] 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.]
[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
[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
[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

2004

[BCM+04] R. Barbuti, S. Cataudella, A. Maggiolo-Schettini, P. Milazzo and A. Troina. A Probabilistic Calculus for Molecular Systems. In Proc. Concurrency Specification and Programming (CS&P'04). 2004. [bib] http://www.di.unipi.it/~milazzo/
[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
[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
[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
[DKNP04] Marie Duflot, Marta Kwiatkowska, Gethin Norman and David Parker. A Formal Analysis of Bluetooth Device Discovery. In T. Margaria and B. Steffen, A. Philippou and M. Reitenspiess (editors), Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), volume TR-2004-6 of Technical Report, pages 268-275, Department of Computer Science, University of Cyprus. November 2004. [ps.gz] [pdf] [bib] [Analyses device discovery in Bluetooth using PRISM.]
[KPZM04] Marta Kwiatkowska, David Parker, Yi Zhang and Rashid Mehmood. Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking. In Proc. 12th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 123-130, IEEE CS Press. October 2004. [ps.gz] [pdf] [bib]
[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]
[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
[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/
[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]
[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]
[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]
[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
[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]
[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.]
[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]
[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.]
[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.]
[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]
[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]
[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]
[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/
[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
[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
[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]
[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
[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]
[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
[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]
[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/
[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]
[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]
[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/
[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]
[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

[Par02] David Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham. 2002. [pdf] [bib]
[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.]
[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
[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]
[KNS02a] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In H. Hermanns and R. Segala (editors), Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 169-187, Springer. July 2002. [ps.gz] [pdf] [bib]
[KM02] M. Kwiatkowska and R. Mehmood. Out-of-Core Solution of Large Linear Systems of Equations arising from Stochastic Modelling. In Proc. PAPM/PROBMIV'02, volume 2399 of LNCS, pages 135-151, Springer-Verlag. July 2002. [ps.gz] [bib]
[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]
[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]
[KNSS02] M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science, 282, pages 101-150. June 2002. [ps.gz] [pdf] [bib]
[Shm02] V. Shmatikov. Probabilistic Analysis of Anonymity. In Proc. 15th IEEE Computer Security Foundations Workshop (CSFW'02), pages 119-128, IEEE CS Press. June 2002. [bib] http://www.cs.utexas.edu/~shmat/index.html
[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.]
[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]
[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.]
[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]
[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.]

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