PRISM Bibliography (external)

The following is a bibliography of external PRISM-related papers. These are all published by authors who are not part of the PRISM team.

See also the lists of papers produced by the PRISM team, selected PRISM papers and the full PRISM bibliography.

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

Sort by: date, type, title, subject

Tool/language connections to PRISM
Extensions and adaptions to PRISM
Case studies using PRISM
Others

632 publications:

Tool/language connections to PRISM (238)

2024

[VDM24] Ivaylo Valkov, Alastair F. Donaldson and Alice Miller. Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking. In Proc. 30th International Symposium on Model Checking of Software (SPIN'24). 2024. [Presents a symmetry reduction method targeting the PRISM modelling language and tool with support for synchronisation-based communication.]
[KKP+24] Ryeonggu Kwon, Gihwon Kwon, Sohee Park, Jiyoung Chang, Suhee Jo, Yeongtong-gu, Gyeonggi-do, Suwon-si. Applying Quantitative Model Checking to Analyze Safety in Reinforcement Learning. IEEE Access. 2024. [Uses PRISM to analyse models learnt by reinforcement learning.]

2023

[Sch23] Georg Friedrich Schuppe. Assumptions in Synthesis: An Approach to Multi-Agent Planning from Spatio-Temporal Specifications. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden. 2023. [Presents decentralised strategy synthesis algorithms for multi-agent systems, including a tool chain that incorporares PRISM-games. ]
[GLHW23] Anna Gautier, Bruno Lacerda, Nick Hawes and Michael J. Wooldridge. Multi-Unit Auctions for Allocating Chance-Constrained Resources. AAAI 2023. In Proc. 37th AAAI Conference on Artificial Intelligence (AAAI'23), pages 11560-11568. 2023. [Proposes methods for chance-constrained multi-agent resource allocation including PRISM as a back-end multi-objective solver.]
[KGK23] Jonis Kiesbye, Kush Grover and Jan Křetínský. Model Checking for Proving and Improving Fault Tolerance of Satellites. In Proc. 2023 IEEE Aerospace Conference. 2023. [Presents an approach for analysing and improving the architecture of spacecraft, with a toolchain that interfaces with PRISM for policy generation.]
[WEAH23] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada and Ichiro Hasuo. Compositional Probabilistic Model Checking with String Diagrams of MDPs. In Proc. International Conference on Computer Aided Verification (CAV'23). 2023. [Presents a compositional approach to probabilistic model checking, with an implementation based on PRISM.]
[DS23] Susmoy Das and Arpit Sharma. On the Use of Model and Logical Embeddings for Model Checking of Probabilistic Systems. In Proc. International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'23). 2023. [Proposes methods for translating between state and action based models, using PRISM to implement and evaluate the framework.]
[GHA+23] Yue Gu, William Hunt, Blair Archibald, Mengwei Xu, Michele Sevegnani and Mohammad D. Soorati. Successful Swarms: Operator Situational Awareness with Modelling and Verification at Runtime. In Proc. 2023 32nd IEEE International Conference on Robot and Human Interactive Communication (RO-MAN). 2023. [Presents formal modelling and verification techniques for robot swarms, building on probabilistic model checking and PRISM.]
[DWG23] J. Andres Diaz-Pace, Rebekka Wohlrab and David Garlan. Supporting the Exploration of Quality Attribute Tradeoffs in Large Design Spaces. In Proc. European Conference on Software Architecture (ECSA'23). 2023. [Proposes methods for tackling large design spaces in software architectures using PRISM as an underlying solver.]
[OMD23] Samir Ouchani, Otmane Ait Mohamed and Mourad Debbabi. An Enhanced Interface-Based Probabilistic Compositional Verification Approach. In Proc. International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS'23). 2023. [Proposes compositional methods for probabilistic verification using PRISM as an underlying engine.]
[BRAJ23] Thom Badings, Licio Romao, Alessandro Abate and Nils Jansen. Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty. In Proc. AAAI'23. 2023. [Develops uncertainty-aware controller synthesis methods for stochastic dynamical models, using PRISM to solve interval MDPs.]
[WLN+23] Xia Wang, Jun Liu, Chris Nugent, Ian Cleland and Yang Xu. Mobile agent path planning under uncertain environment using reinforcement learning and probabilistic model checking. Knowledge-Based Systems. 2023. [Presents a mobile agent path planning framework that integrates verification via PRISM.]
[ABD+23] Yamine Aït-Ameur, Sergiy Bogomolov, Guillaume Dupont, Alexei Iliasov, Alexander Romanovsky and Paulius Stankaitis. A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems. Formal Aspects of Computing. 2023. [Presents a formal development methodology for railway signalling systems, including the use of PRISM for probabilistic verification.]
[CBDK23] Philipp Chrszon, Christel Baier, Clemens Dubslaff and Sascha Klüppelholz. Interaction detection in configurable systems – A formal approach featuring roles. Journal of Systems and Software. 2023. [Proposes a role-based compositional modelling framework for software systems, using a translation to the PRISM language.]
[FKO03] I. A. Fedotov, A. S. Khritanko and M. D. Obidare. Automated Verification of Multi-Party Agreements and Scheduling of Sending Messages in Distributed Ledger Systems. Programming and Computer Software, 49. 2023. [Proposes an approach to analyse multi-party agreements for distributed ledger systems based on PRISM.]
[ACSX23b] Blair Archibald, Muffy Calder, Michele Sevegnani and Mengwei Xu. Quantitative modelling and analysis of BDI agents. Software and Systems Modeling , Springer. 2023. [Defines a probabilistic extension to the Conceptual Agent Notation for probabilistic Belief-Desire-Intention models, solved using PRISM. ]
[FCGA23] Xinwei Fang, Radu Calinescu, Simos Gerasimou and Faisal Alhwikem. Fast Parametric Model Checking With Applications to Software Performability Analysis. IEEE Transactions on Software Engineering. 2023. [Presents an efficient approach to parametric employing calls to probabilistic model checkers including PRISM.]

2022

[KGAK22] Jonis Kiesbye, Kush Grover, Pranav Ashok and Jan Křetínský. Planning via model checking with decision-tree controllers. In Proc. International Conference on Robotics and Automation (ICRA'22). 2022. [Uses PRISM within a toolchain for planning with decision-tree controller generation.]
[RCP+22] Joshua Riley, Radu Calinescu, Colin Paterson, Daniel Kudenko and Alec Banks. Assured Deep Multi-Agent Reinforcement Learning for Safe Robotic Systems. In Proc. International Conference on Agents and Artificial Intelligence (ICAART'22). 2022. [Uses quantitative verification within a multi-agent reinforcement learning setup, deploying PRISM for policy synthesis.]
[OOT22] Lisa Oakley, Alina Oprea and Stavros Tripakis. Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems. In Proc. IEEE 35th Computer Security Foundations Symposium (CSF'22). 2022. [Presents a framework for adversarial robustness in Markov models, using PRISM to perform model checking.]
[TAL22] Anne Theurkauf, Nisar Ahmed and Morteza Lahijanian. Pareto Optimal Strategies for Event-triggered Estimation. In Proc. IEEE 61st Conference on Decision and Control (CDC'22). 2022. [Proposes techniques for analysing resource-performance trade-offs in a distributed sensor network using PRISM and PRISM-games.]
[ACSX22] Blair Archibald, Muffy Calder, Michele Sevegnani and Mengwei Xu. Verifying BDI Agents in Dynamic Environments. In Proc. 34th International Conference on Software Engineering and Knowledge Engineering (SEKE'22). 2022. [Proposes a framework for verifying Belief-Desire-Intention (BDI) agents in dynamic environments, building on PRISM.]
[WMV22] Rebekka Wohlrab; Rômulo Meira-góes and Michael Vierhauser. Run-Time Adaptation of Quality Attributes for Automated Planning. In Proc. International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'22). 2022. [Proposes automated planning techniques with run-time adaptation of quality attributes, using PRISM for policy synthesis.]
[RCP+22b] Joshua Riley, Radu Calinescu, Colin Paterson Daniel Kudenko, Alec Banks. Assured Multi-agent Reinforcement Learning with Robust Agent-Interaction Adaptability. In Proc. 26th International Conference on Knowledge-Based and Intelligent Information & Engineering Systems (KES'22). 2022. [Presents an extension to the assured multi-agent reinforcement learning approach with abstractions built as PRISM models. ]
[VCC22] Gricel Vázquez, Radu Calinescu and Javier Cámara. Scheduling of Missions with Constrained Tasks for Heterogeneous Robot Systems. In Proc. FMAS/ASYDE@SEFM. 2022. [Presents an approach to multi-robot task allocation and scheduling with a connection to PRISM for model evaluation.]
[ACPM22] Naif Alasmari, Radu Calinescu, Colin Paterson and Raffaela Mirandola. Quantitative verification with adaptive uncertainty reduction. Journal of Systems and Software. 2022. [Presents an approach called VERACITY for adaptive uncertainty reduction when verifying Markov chains, with a connection to PRISM.]
[GCD+22] Mario Gleirscher, Radu Calinescu, James Douthwaite, Benjamin Lesage, Colin Paterson, Jonathan Aitken, Rob Alexander and James Law. Verified Synthesis of Optimal Safety Controllers for Human-Robot Collaboration. Science of Computer Programming. 2022. [Presents a tool-supported approach for verified synthesis of safety controllers, using PRISM for policy construction.]
[ACSX22b] Blair Archibald, Muffy Calder, Michele Sevegnani and Mengwei Xu. Modelling and verifying BDI agents with bigraphs. Science of Computer Programming. 2022. [Encodes Belief-Desire-Intention (BDI) programming languages using bigraphs and exports them to PRISM for solution.]
[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.]

2021

[FCGA21] Xinwei Fang, Radu Calinescu, Simos Gerasimou and Faisal Alhwikem. Fast Parametric Model Checking through Model Fragmentation. In Proc. International Conference on Software Engineering (ICSE'21). 2021. [Presents an efficient approach to parametric employing calls to probabilistic model checkers including PRISM.]
[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.]
[BZK21] Matthew L. Bolton, Xi Zheng and Eunsuk Kang. A formal method for including the probability of erroneous human task behavior in system analyses. Reliability Engineering & System Safety, 213. 2021. [Proposes formal methods to reason about human error in computer systems, including a connection to PRISM for probabilistic verification.]
[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.]
[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.]
[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.]
[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.]
[Maz21] Łukasz Mazurek. EthVer: Formal Verification of Randomized Ethereum Smart Contracts. In International Conference on Financial Cryptography and Data Security (FC'21) Workshops. 2021. [Develops a tool for formal verification of randomised Ethereum smart contracts, building upon 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.]
[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.]
[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.]
[RCP+21] Joshua Riley, Radu Calinescu, Colin Paterson Daniel Kudenko, Alec Banks. Utilising Assured Multi-Agent Reinforcement Learning within Safety-Critical Scenarios. In Proc. 25th International Conference on Knowledge-Based and Intelligent Information & Engineering Systems (KES'21). 2021. [Presents an approach called assured multi-agent reinforcement learning with abstractions built as PRISM models. ]
[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.]
[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. ]
[ACSX21] Blair Archibald, Muffy Calder, Michele Sevegnani, Mengwei Xu. Observable and Attention-Directing BDI Agents for Human-Autonomy Teaming. In Proc. Third Workshop on Formal Methods for Autonomous Systems (FMAS'21). 2021. [Proposes methods for formal modelling and analysis of human-autonomy teaming scenarios, using PRISM as an underlying solver.]
[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.]
[ACSX21b] Blair Archibald, Muffy Calder, Michele Sevegnani and Mengwei Xu. Probabilistic BDI Agents: Actions, Plans, and Intentions. In Proc. International Conference on Software Engineering and Formal Methods (SEFM'21). 2021. [Defines a probabilistic extension to the Conceptual Agent Notation for probabilistic Belief-Desire-Intention models, solved using PRISM.]
[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.]
[ZLZ+21] Mingyue Zhang, Jialong Li, Haiyan Zhao, Kenji Tei, Shinichi Honiden and Zhi Jin. A Meta Reinforcement Learning-based Approach for Self-Adaptive System. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'21). 2021. [Presents a machine learning based framework for self-learning adaptive systems, including the use of PRISM-games. ]
[Ouc21] Samir Ouchani. A security policy hardening framework for Socio-Cyber-Physical Systems. Journal of Systems Architecture, 119. 2021. [Proposes techniques for analysing the security of socio-cyber-physical systems, with underlying verification tasks performed by PRISM.]
[BH21] Paolo Ballarini and András Horváth. Formal analysis of production line systems by probabilistic model checking tools. In Proc. 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'21). 2021. [Presents a framework for performance analysis of production line systems using probabilistic model checking and PRISM. ]
[SIK+21] Paulius Stankaitis, Alexei Iliasov, Tsutomu Kobayashi, Yamine Ait-Ameur, Fuyuki Ishikawa and Alexander Romanovsky. A refinement-based development of a distributed signalling system. Formal Aspects of Computing. 2021. [Presents a formal development methodology for railway signalling systems, including the use of PRISM for probabilistic verification.]
[CAG21] Radu Calinescu, Naif Alasmari and Mario Gleirscher. Maintaining driver attentiveness in shared-control autonomous driving. In Proc. International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'21). 2021. [Presents a control loop for improving driver attentiveness with controllers synthesised via PRISM models.]
[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.]

2020

[RMT+20] Michael Raitza, Steffen Märcker, Jens Trommer, André Heinzig, Sascha Klüppelholz, Christel Baier and Akash Kumar. Quantitative Characterization of Reconfigurable Transistor Logic Gates. IEEE Access. 2020. [Presents formal analysis techniques for logic gates using probabilistic model checking and a toolchain based on PRISM.]
[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.]
[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.]
[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.]
[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.]
[ZBDB20] Xi Zheng Matthew L. Bolton, Christopher Daly and Elliot Biltekoff. The development of a next-generation human reliability analysis: Systems analysis for formal pharmaceutical human reliability (SAFPH℞). Reliability Engineering & System Safet7, 202. 2020. [Uses probabilistic model checking and PRISM to predict medication error rates and explore interventions in pharmacy dispensing procedures. ]
[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.]
[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.]
[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.]
[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.]
[RCCS20] Nelson Rosa, David Cavalcanti, Gláucia Campos and André Silva. Adaptive middleware in go - a software architecture-based approach. Journal of Internet Services and Applications. 2020. [Presents and approach to developing adaptive middleware, including a connection to PRISM for quantitative analysis.]
[DMBJ20b] Clemens Dubslaff, Andrey Morozov, Christel Baier and Klaus Janschek. Reduction Methods on Probabilistic Control-flow Programs for Reliability Analysis. In Proc. 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference. 2020. [Presents automated reduction techniques for PRISM modelling language descriptions.]
[Cam20] Javier Cámara. HaiQ: Synthesis of Software Design Spaces with Structural and Probabilistic Guarantees. In Proc. IEEE/ACM 8th International Conference on Formal Methods in Software Engineering (FormaliSE'20). 2020. [Presents a tool, HaiQ, for formal analysis of software desings, including PRISM as a backend.]

2019

[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.]
[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.]
[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.]
[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. ]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[RCC19] Nelson S. Rosa, Gláucia M. M. Campos and David J.M. Cavalcanti. Lightweight formalisation of adaptive middleware. Journal of Systems Architecture. 2019. [Proposes an approach to developing adaptive middleware that integrates PRISM for performing probabilistic verification.]

2018

[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.]
[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.]
[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.]
[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.]
[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.]
[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. ]
[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.]
[LJ18] Nian-Ze Lee and Jie-Hong R. Jiang. Towards Formal Evaluation and Verification of Probabilistic Design. IEEE Transactions on Computers, 67(8), pages 1202-1216, IEEE. 2018. [Uses PRISM as part of a framework to verify approximate and probabilistic designs for circuits.]
[CDKB+18] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. ProFeat: Feature-oriented Engineering for Family-based Probabilistic Model Checking. Formal Aspects of Computing, volume, 30(1), pages 45-75. 2018. [Presents the ProFeat tool for feature-oriented modelling and feature-aware analysis, incorporating PRISM.]

2017

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

2016

[SC16] Michele Sevegnani and Muffy Calder. BigraphER: rewriting and analysis engine for bigraphs. In Proc. 28th International Conference on Computer Aided Verification (CAV'16). 2016. [Presents a suite of tools for working with bigraphs, including export to PRISM for probabilistic bigraphs.]
[PWHA16] Elizabeth Polgreen, Viraj B. Wijesuriya, Sofie Haesaert and Alessandro Abate. Data-Efficient Bayesian Verification of Parametric Markov Chains. In Proc. 13th International Conference on Quantitative Evaluation of Systems (QEST'16). 2016. [Presents Bayesian methods for probabilistic model checking of Markov chains, implemented using PRISM's parametric model checking functionality.]
[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.]
[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.]
[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.]
[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.]
[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.]
[CDKB16] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat. In Proc. 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), volume 9633 of LNCS, pages 287-304, Springer. 2016. [Proposes a formalism for modelling families of probabilistic systems with differing features and a tool for their analysis, which connects to PRISM through model translations.]
[MRAAB16] Danilo Filgueira Mendonça, Genaína Nunes Rodriguesa, Raian Alib, Vander Alvesa and Luciano Baresi. GODA: A goal-oriented requirements engineering framework for runtime dependability analysis. Information and Software Technology, 80, pages 245–264, Elsevier. 2016. [Proposes GODA, a goal-oriented requirements engineering framework for runtime dependability analysis, which uses probabilistic model checking and PRISM for underlying analysis. ]

2015

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

2014

[HBHS14] Fenglin Han, Jan Olaf Blech, Peter Herrmann and Heinz Schmidt. Towards Verifying Safety Properties of Real-Time Probabilistic Systems. In Proc. Formal Engineering Approaches to Software Components and Architectures (FESCA'14), EPTCS. 2014. [Presents an extension of the Reactive Blocks tool set for analysing probabilistic real-time systems, through a connection to PRISM.]
[GPST14] Carlo Ghezzi, Mauro Pezzè, Michele Sama and Giordano Tamburrelli. Mining Behavior Models from User-Intensive Web Applications. In Proc. ICSE'14. 2014. [Proposes techniques to infer probabilistic behaviour models from web application logs and analyses the models using PRISM.]
[RLK14] Pedro Rodrigues, Emil Lupu and Jeff Kramer. LTSA-PCA: tool support for compositional reliability analysis. In 36th International Conference on Software Engineering, ICSE '14, Companion Proceedings, pages 548-551. 2014. [Presents an extension of the LTSA model checker for compositional reliability analysis, which uses a connection to PRISM. ]
[KH14] Koichi Kobayashi and Kunihiko Hiraishi. Verification and Optimal Control of Context-Sensitive Probabilistic Boolean Networks Using Model Checking and Polynomial Optimization. The Scientific World Journal. 2014. [Presents various techniques for analysing probabilistic Boolean networks, including one that uses probabilistic model checking and PRISM.]
[SR14] Guoxin Su and David S. Rosenblum. Perturbation analysis of stochastic systems with empirical distribution parameters. In Proc. 36th International Conference on Software Engineering (ICSE'14). 2014. [Proposes techniques for analysing peturbations in probabilistic models using parametric model checking and a connection to PRISM.]
[LJ14] Nian-Ze Lee and Jie-Hong R. Jiang. Towards formal evaluation and verification of probabilistic design. In Proc. 2014 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'14). 2014. [Uses PRISM as part of a framework to verify approximate and probabilistic designs for circuits.]
[Kon14] Savas Konur. Towards Light-Weight Probabilistic Model Checking. Journal of Applied Mathematics. 2014. [Proposes a framework for non-experts to specify models and queries for probabilistic model checking, connecting to PRISM and other tools.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[OMD14] Samir Ouchani, Otmane Aït Mohameda and Mourad Debbabi. A property-based abstraction framework for SysML activity diagrams. Knowledge-Based Systems, 6, pages 328-343. January 2014. [Presents methods to abstract and verify SysML activity diagrams using PRISM as a back-end.]

2013

[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.]
[KJR13] Radu Calinescu, Kenneth Johnson and Yasmin Rafiq. Developing Self-Verifying Service-Based Systems. In Proc. 28th IEEE/ACM International Conference on Automated Software Engineering (ASE'13), IEEE. 2013. [Describes a self-verifying framework for service-based systems, including PRISM as a backend solver.]
[SGO13] Simon Struck, Matthias Gudemann and Frank Ortmeier. Efficient Optimization of Large Probabilistic Models. Journal of Systems and Software. 2013. [Presents a framework for modelling, analysis and optimization of safety critical systems, which connects to PRISM.]
[ZREF13] Fokion Zervoudakis, David S. Rosenblum, Sebastian Elbaum and Anthony Finkelstein. Cascading Verification: An Integrated Method for Domain-Specific Model Checking. In Proc. 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE'13), pages 400-410 , ACM. 2013. [Proposes a domain-specific model checking framework, including PRISM as an underlying solver.]
[FBZ13] João Franco, Raul Barbosa and Mário Zenha Rela. Reliability analysis of software architecture evolution. In Proc. Latin-American Symposium on Dependable Computing (LADC'13). 2013. [Analyses quality attributes of software architectures by translating an architecture design language into PRISM. ]
[PTA13] Anna Philippou, Mauricio Toro and Margarita Antonaki. Simulation and Verification for a Process Calculus for Spatially-explicit Ecological Models. Scientific Annals of Computer Science, 23(1), pages 119–167. 2013. [Develops a stochastic process algebra for locations/populations called PALPS, with a translation into PRISM for probabilistic model checking.]
[JCK13] Kenneth Johnson, Radu Calinescu and Shinji Kikuchi. An Incremental Verification Framework for Component-Based Software Systems. In Proc. 16th International ACM Sigsoft symposium on Component-based software engineering (CBSE'13), pages 33-42. 2013. [Presents a framework for the efficient reverification of component-based software system, with a software prototype built on top of PRISM.]
[RBC+13] Neha Rungta, Guillaume Brat, William J. Clancey, Charlotte Linde, Franco Raimondi, Chin Seah and Michael Shafto. Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems. In Proc. International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
[HRRS13] Josie Hunter, Franco Raimondi, Neha Rungta and Richard Stocker. A synergistic and extensible framework for multi-agent system verification. In Proc. International conference on Autonomous Agents and Multi-Agent Systems (AAMAS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
[LFL13] Florian Leitner-Fischer and Stefan Leue. On the Synergy of Probabilistic Causality Computation and Causality Checking. In Proc. 20th International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 246-263, Springer. 2013. [Develops an approach for causality checking, which uses PRISM for some of the underlying computations.]
[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.]
[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.]
[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.]

2012

[Kum12] Jayanand Asok Kumar. Statistical Guarantees of Performance for RTL Designs. Ph.D. thesis, University of Illinois at Urbana-Champaign. 2012. [bib]
[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.
[OGLS12] Frank Ortmeier, Matthias Gudemann, Michael Lipaczewski and Simon Struck. Unifying Probabilistic and Traditional Formal Model Based Analysis. In Proc. MBEES. 2012.
[GMS+12] Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe Ferri and Edson Watanabe. Constructive model-based analysis for safety assessment. International Journal on Software Tools for Technology Transfer (STTT). 2012. [Uses PRISM in a quantitative safety assessment framework via model translation from Simulink.]
[JD12] Yosr Jarraya and Mourad Debbabi. Formal Specification and Probabilistic Verification of SysML Activity Diagrams. In Proc. 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12). 2012. [Presents a framework for probabilistic verification of SysML activity diagrams via a translation to PRISM.]
[MMAG12] Indika Meedeniya, Irene Moser, Aldeida Aleti and Lars Grunske. Evaluating Probabilistic Models with Uncertain Model Parameters. Software and Systems Modelling, Springer. 2012. [Proposes techniques to evaluate probabilistic models with uncertainty, using PRISM as a back-end solution engine.]
[KG12] Christian Krause and Holger Giese. Probabilistic Graph Transformation Systems. In Proc. 6th International Conference on Graph Transformations (ICGT'12), pages 311-325. 2012. [Proposes techniques to analyse probabilistic graph transformation systems, using the tools HENSHIN and PRISM.]
[VK12] Mahsa Varshosaz and Ramtin Khosravi. Modeling and Verification of Probabilistic Actor Systems Using pRebeca. In Proc. 14th International Conference on Formal Engineering Methods, Formal Methods and Software Engineering (ICFEM'12), volume 7635 of LNCS, Springer. 2012. [Uses PRISM to analyse systems described in a probabilistic actor-based modelling language called pRebeca.]
[HS12] Luke Herbert and Robin Sharp. Using stochastic model checking to provision complex business services. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 98-105, IEEE. 2012. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows. Illustrated on a medical case study.]
[LSO12] Michael Lipaczewski, Simon Struck and Frank Ortmeier. Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 159-166. 2012. [Presents tool support for the safety analysis modelling language (SAML), which connects to PRISM for probabilistic verification.]
[SLOG12] Simon Struck, Michael Lipaczewski, Frank Ortmeier and Matthias Güdemann. Multi-objective Optimization of Formal Specifications. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 201-208. 2012. [Develops model-based optimisation methods which connect to PRISM for model analysis.]
[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.]

2011

[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]
[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]
[STTT11] Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi and Kazuko Takahashi. Probabilistic Symmetry Reduction for a System with Ring Buffer. IEICE Transactions, 94-D(5), pages 967-975. 2011. [bib]
[KLV11] Jayanand Asok Kumar, Lingyi Liu and Shobha Vasudevan. Scaling Probabilistic Timing Verification of Hardware Using Abstractions in Design Source Code. In Proc. 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD'11). 2011. [bib]
[JRC11] Kenneth Johnson, Simon Reed and Radu Calinescu. Specification and Quantitative Analysis of Probabilistic Cloud Deployment Patterns. In Proc. 7th Haifa Verification Conference (HVC'11). 2011. [bib]
[AB11] R. Abo and K. Barkaoui. A performability analysis of mobile wireless sensor networks with probabilistic model checking. In Proc. Wireless Advanced (WiAd'11), pages 283-288. 2011.
[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.
[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.

2010

[RMH10] C. Rohr, W. Marwan and M. Heiner. Snoopy - A unifying Petri net framework to investigate biomolecular networks. Bioinformatics, 26(7), pages 974-975. 2010. [bib]
[ZYXL10] Yefei Zhao, Zongyuan Yang, Jinkui Xie and Qiang Liu. Quantitative Analysis of System Based on Extended UML State Diagrams and Probabilistic Model Checking. Journal of Software, 5(7), pages 793-800. 2010. [bib]
[AA10] M. Akbarzadeh and M. Azgomi. A framework for probabilistic model checking of security protocols using coloured stochastic activity networks and PDETool. In Proc. 5th International Symposium on Telecommunications (IST'10), pages 210-215. 2010. [bib]
[Jar10] Yosr Jarraya. Verification and Validation of UML and SysML Based Systems Engineering Design Models. Ph.D. thesis, Concordia University. 2010. [bib]
[HKL+10] B. Haverkort, M. Kuntz, F. Leitner-Fischer, A. Remke and S. Roolvink. Probabilistic Verification of Architectural Software Models using SoftArc and Prism. In Proc. ESREL Annual Conference. 2010. [bib]
[GO10b] Matthias Gudemann and Frank Ortmeier. A Framework for Qualitative and Quantitative Formal Model-Based Safety Analysis. In Proc. 12th IEEE High Assurance Systems Engineering Symposium (HASE'10), pages 132-141. 2010.

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]
[ACvdM+09] F. Arbab, T. Chothia, R. van der Mei, M. Sun, Y.-J. Moon and C. Verhoef. From Coordination to Stochastic Models of QoS. In Proc. 11th international conference on Coordination Models and Languages (Coordination'09). 2009. [bib]
[BLMS09] R. Barbuti, F. Levi, P. Milazzo and G. Scatena. Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates. In 3rd International Workshop on Reachability Problems (RP'09). 2009. [bib]
[Ndu09] U. Ndukwu. Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems. In Proc. Workshop on Quantitative Formal Methods (QFM'09). 2009. [bib]
[HH09] A. Hartmanns and H. Hermanns. A Modest Approach to Checking Probabilistic Timed Automata. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). To appear. September 2009. [bib]
[AMMKQ09] F. Arbab, S. Meng, Y.-J. Moon, M. Kwiatkowska and H. Qu. Reo2MC: a Tool Chain for Performance Analysis of Coordination Models. In Hans van Vliet, Valérie Issarny (editor), The 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 287-288, ACM. August 2009. [pdf] [bib] [Presents a tool chain for analysing Stochastic Reo models, incorporating PRISM.]

2008

[AGM08] D. Ardagna, C. Ghezzi and R. Mirandola. Model Driven QoS Analyses of Composed Web Services. In Proc. ServiceWave 2008, volume 5377 of LNCS, pages 299-311, Springer. 2008. [bib]
[GGMT08] S. Gallotti, C. Ghezzi, R. Mirandola and G. Tamburrelli. Quality Prediction of Service Compositions through Probabilistic Model Checking. In Proc. 4th International Conference on the Quality of Software-Architectures (QoSA'08), volume 5281 of LNCS, pages 119-134, Springer. 2008. [bib]
[CGGH08] F. Ciocchetta, S. Gilmore, M. L. Guerriero and J. Hillston. Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems. In Proc. 3rd International Workshop on Practical Applications of Stochastic Modelling (PASM'08), volume 232 of ENTCS, pages 17-38. 2008. [bib]

2007

[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/
[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
[MM07] A. McIver and C. Morgan. Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic, 8(1). 2007. [bib]
[BGRC+07] F. Bernardini, M. Gheorghe, F. Romero-Campero and N. Walkinshaw. A Hybrid Approach to Modelling Biological Systems. In Proc. 8th Workshop on Membrane Computing, volume 4860 of Lecture Notes in Computer Science, Springer. 2007. [bib] http://www.dcs.shef.ac.uk/~nw/Publications.html
[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]

2006

[McI06] A. McIver. Quantitative refinement and model checking for the analysis of probabilistic systems. In Proc. Formal Methods (FM'06). To appear. 2006. [bib]
[CDDS06] D. Cerotti, D. D'Aprile, S. Donatelli and J. Sproston. Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools. In Proc. 6th International Conference on Application of Concurrency to System Design (ACSD'06), IEEE Computer Society Press. 2006. [bib]
[RCGB+06] Francisco José Romero-Campero, Marian Gheorghe, Luca Bianco, Dario Pescini, Mario J. Péerez-Jiménez and Rodica Ceterchi. Towards Probabilistic Model Checking on P Systems Using PRISM. In Workshop on Membrane Computing, pages 477-495. 2006.
[DM06] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Model Checking using Generic Representatives. In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of LNCS, pages 9-23, Springer. October 2006. [bib] http://www.dcs.gla.ac.uk/people/personal/alice/publications.html
[GRV06] U. Glasser, S. Rastkar and M. Vajihollahi. Computational Modeling and Experimental Validation of Aviation Security Procedures. In Proc. Intelligence and Security Informatics (ISI'06) . May 2006. http://fas.sfu.ca/pub/cs/techreports/2006/CMPT2006-02.pdf

2005

[Hec05] R. Heckel. Stochastic Analysis of Graph Transformation Systems: A Case Study in P2P Networks. In Proc. 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC'05), volume 3722 of LNCS, Springer. October 2005. http://www.cs.le.ac.uk/people/rh122/papers/2005/Hec05ICTAC.pdf
[DM05] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Systems. In Proc. 12th workshop on Automated Reasoning, pages 17-18. July 2005. [bib] http://www.dcs.gla.ac.uk/people/personal/alice/publications.html
[BCM+05] R. Barbuti, S. Cataudella, A. Maggiolo-Schettini, P. Milazzo and A. Troina. A Probabilistic Model for Molecular Systems. Fundamenta Informaticae, 67(1-3), pages 13-27. July 2005. [bib] http://www.di.unipi.it/~milazzo/
[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/
[GW05] M. Goldsmith and P. Whittaker. A CSP Frontend for Probabilistic Tools. Technical report FORWARD Deliverable D14, Formal Systems (Europe Ltd). June 2005. [bib] http://www.forward-project.org.uk/PDF_Files/D14.pdf

2004

[KSW04a] M. Kuntz, M. Siegle and E. Werner. Symbolic Performance and Dependability Evaluation with the Tool CASPA. In Proc. 1st European Performance Engineering Workshop (EPEW'04), FORTE'04 workshop, volume 3236 of LNCS, pages 293-307, Springer-Verlag. 2004. [bib] http://fakinf.informatik.unibw-muenchen.de/~msiegle/own.html
[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/
[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
[KSW04b] M. Kuntz, M. Siegle and E. Werner. CASPA: A Tool for Symbolic Performance and Dependability Evaluation. In Supplemental Volume of Proc. of Int. Conf. on Dependable Systems and Networks (DSN'04), pages 90-91. 2004. http://fakinf.informatik.unibw-muenchen.de/~msiegle/own.html
[GHHK04] S. Gilmore, V. Haenel, J. Hillston and L. Kloul. PEPA nets in practice: Modelling a decentralised peer-to-peer emergency medical application. In Proc. 1st European Performance Evaluation Workshop (EPEW'04), volume 3236 of LNCS, pages 262-277, Springer-Verlag. October 2004. http://www.dcs.ed.ac.uk/home/stg/
[HLM04] R. Heckel, G. Lajios and S. Menge. Stochastic Graph Transformation Systems. In Proc. 2nd International Conference on Graph Transformations (ICGT'04), volume 3256 of LNCS, pages 210-225, Springer. October 2004. [bib] http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3256&spage=210
[DDS04] D. D'Aprile, S. Donatelli and J. Sproston. CSL Model Checking for the GreatSPN Tool. In C. Aykanat, T. Dayar and I. Korpeoglu (editors), International Symposium on Computer and Information Sciences, volume 3280 of Lecture Notes in Computer Science, pages 543-552, Springer Verlag. 2004. http://www.di.unito.it/~sproston/Research/research.html

2003

[GHB+03] M. Gribaudo, A. Horvath, A. Bobbio, E. Tronci, E. Ciancamerla and M. Minichino. Fluid Petri Nets and Hybrid Model-checking: A Comparative Case Study. Reliability Engineering and System Safety, 81, pages 239-257. 2003. [bib] http://www.mfn.unipmn.it/~bobbio/BIBLIO/bliagg.html
[Jan03] D. Jansen. Extensions of statecharts with probability, time, and stochastic timing. Ph.D. thesis, Universiteit Twente. October 2003. http://depend.cs.uni-sb.de/?id=200
[JPS03] J. Jayaputera, I. Poernomo, H. Schmidt. Timed Probabilistic Reasoning on UML Specialization for Fault Tolerant Component Based Architectures. In Proc. Specification and Verification of Component-Based Systems (SAVCBS'03), Workshop at ESEC/FSE'03. September 2003. http://www.cs.iastate.edu/~leavens/SAVCBS/2003/papers/index.shtml
[GK03] S. Gilmore and L. Kloul. A unified tool for performance modelling and predicition. In Proc. 22nd International Conference on Computer Safety, Reliability and Security (SAFECOMP'03), volume 2788 of LNCS, pages 179-192, Springer-Verlag. September 2003. http://www.dcs.ed.ac.uk/home/stg/
[GHKR03] S. Gilmore, J. Hillston, L. Kloul and M. Ribaudo. Performance modelling with PEPA nets and PRISM. In Proc. 2nd Workshop on Process Algebra and Stochastically Timed Activities (PASTA Secondi Piatti), pages 23-39. June 2003. http://www.dcs.ed.ac.uk/home/stg/

2002

[JHK02] D. Jansen, H. Hermanns and J.-P. Katoen. A Probabilistic Extension of UML Statecharts Specification and Verification. In Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 355-374, Springer-Verlag. September 2002. http://depend.cs.uni-sb.de/?id=200

Extensions and adaptions to PRISM (63)

2024

[ElS24] Ingy ElSayed-Aly. Safe Sequential Decision Making in Uncertain Environments. Ph.D. thesis, University of Virginia. 2024. https://libraetd.lib.virginia.edu/public_view/x346d566k [Develops methods for safe sequential decision making, including distributional extensions of probabilistic model checking implemented in PRISM.]
[LSV24] Cosimo Laneve, Sergio Solmonte and Adele Veschetti. A Stochastic Analysis of the Gasper Protocol. In Proc. IEEE International Conference on Pervasive Computing and Communications Workshops. 2024. [Analyses Ethereum's Proof of Stake consensus protocol, Gasper, using an extension of PRISM.]
[MCA24] Roberto Metere, Ricardo Melo Czekster and Luca Arnaboldi. Enhancing Expressiveness in Stochastic Modelling of Cyber-Physical Systems. In Proc. 13th Mediterranean Conference on Embedded Computing (MECO'24). 2024. [Proposes an extension of the PRISM language for modelling cyber-physical systems.]

2023

[BDG+23] Stefano Bistarelli, Rocco De Nicola, Letterio Galletta, Cosimo Laneve, Ivan Mercanti and Adele Veschetti. Stochastic modeling and analysis of the bitcoin protocol in the presence of block communication delays. Concurrency and Computation: Practice and Experience, 35. 2023. [Uses an extended version of PRISM to analyse a bitcoin blockchain protocol.]
[MC23] Chunyan Mu and David Clark. Verifying Opacity Properties in Security Systems. IEEE Transactions on Dependable and Secure Computing , 20. 2023. [Proposes an opacity based security verification framework, implemented as an extension of PRISM.]
[GLMV03] Letterio Galletta, Cosimo Laneve, Ivan Mercanti and Adele Veschetti. Resilience of Hybrid Casper Under Varying Values of Parameters. Distributed Ledger Technologies: Research and Practice, 2(1), pages 1-25. 2023. [Develops an extension of PRISM for verifying an Ethereum blockchain protocol.]
[BKK+23] Christel Baier, Stefan Kiefer, Joachim Klein, David Muller and James Worrell. Markov chains and unambiguous automata. Journal of Computer and System Sciences. 2023. [Presents techniques for model checking Markov chains against unambiguous automata, implemented as an extension of PRISM.]

2022

[Wei22] Maximilian Weininger. Solving Stochastic Games Reliably. Ph.D. thesis, Technischen Universitat Munchen. 2022. [Proposes a variety of techniques for solving and verifying stochastic games, including implementations in an extension of PRISM-games.]
[MKI22] Mohammadsadegh Mohagheghi, Jaber Karimpour and Ayaz Isazadeh. Improving Modified Policy Iteration for Probabilistic Model Checking. Computer Science. 2022. [Investigates the use of modified policy iteration for probabilistic model checking, implemented as an extension of 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.]
[KRSW02] Jan Kretinsky, Emanuel Ramneantu, Alexander Slivinskiy and Maximilian Weininger. Comparison of algorithms for simple stochastic games. Information and Computation, 289, Part B. 2022. [Investigates existing and novel techniques for solving turn-based stochastic games, using an extension of PRISM-games.]
[LP22] Alessio Lomuscio and Edoardo Pirovano. A counter abstraction technique for verifying properties of probabilistic swarm systems. Artificial Intelligence, 305. 2022. [bib] [Presents techniques for verification of probabilistic swarm systems developed as an extension of PRISM. ]

2021

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

2020

[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.]
[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.]
[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.]
[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.]
[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. ]
[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.]
[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.]
[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.]
[KRSW20] Jan Kretinsky, Emanuel Ramneantu, Alexander Slivinskiy and Maximilian Weininger. Comparison of algorithms for simple stochastic games. In Proc. GandALF'20. 2020. [bib] [Investigates existing and novel techniques for solving turn-based stochastic games, using an extension of PRISM-games.]
[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.]
[EWP20] Mahmoud Elfar, Yu Wang and Miroslav Pajic. Context-Aware Temporal Logic for Probabilistic Systems. In Proc. Automated Technology for Verification and Analysis (ATVA'20). 2020. [Considers model checking for a novel context-aware probabilistic temporal logic, implemented as an extension of PRISM-games.]
[CMK20] Javier Cámara, Henry Muccini and Karthik Vaidhyanathan. Quantitative Verification-Aided Machine Learning: A Tandem Approach for Architecting Self-Adaptive IoT Systems. In Proc. IEEE International Conference on Software Architecture (ICSA'20). 2020. [Presents techniques for proactive self-adaptation, combining machine learning and probabilistic model checking and building on PRISM.]

2019

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

2018

[BCD+18] Christel Baier, Philipp Chrszon, Clemens Dubslaff, Joachim Klein and Sascha Klüppelholz. Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination. In It's All About Coordination. Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab, volume 10865 of LNCS, pages 38-56, Springer. 2018. [Presents an extension of PRISM with multi-action models to analyse exogenous coordination.]
[LP18] Alessio Lomuscio and Edoardo Pirovano. Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems. In Proc. 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI'18), AAAI Press. 2018. https://www.ijcai.org/proceedings/2018/0056.pdf [Proposes verification techniques for probabilistic swarm systems, including an implementation that uses PRISM.]
[KBC+18] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer, 20(2), pages 179-194. 2018. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements.]

2017

[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.]
[BKKW17] Christel Baier, Joachim Klein, Sascha Kluppelholz and Sascha Wunderlich. Maximizing the Conditional Expected Reward for Reaching the Goal. In In Proc. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Springer. 2017. [Introduces novel techniques for computing conditional expected rewards in MDPs, implemented in an extension of PRISM.]
[KBC+17] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer. 2017. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements.]

2016

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

2015

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

2013

[Tsa13] Tony Tsang. Performance Analysis for QoS-Aware Two- Layer Scheduling in LTE Networks. International Journal of Emerging Trends & Technology in Computer Science (IJETTCS), 2(2). 2013. [Uses an extension of PRISM's simulator to solve scheduling and resource allocation problems.]
[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.]

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. [Presents new methods for GPU-based probabilistic model checking, implemented as an extension of 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.]
[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.]
[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.]
[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 built with PRISM and an extension of it.]

2011

[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]
[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]
[BESW11] Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski and Anton Wijs. Parallel probabilistic model checking on general purpose graphics processors. International Journal on Software Tools for Technology Transfer (STTT). 2011. [Presents techniques for parallel probabilistic model checking on GPUs, implemented as an extension of PRISM.]

2010

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

2009

[HHWZ09] H. Hermanns, E. M. Hahn, B. Wachter and L. Zhang. Time-bounded model checking of infinite-state continuous-time Markov chains. Fundamenta Informaticae, 95(1), pages 129-155. 2009. [bib]
[BGH09] A. Basu, A. Ghosh and R. He. Approximate Probabilistic Model Checking Using Bounded Until Properties. In Proc. 11th International Conference on Formal Engineering Methods (ICFEM'09),. 2009. [bib]
[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] [Presents techniques for parallel probabilistic model checking on GPUs, implemented as an extension of PRISM. ]
[Dwo09] H. Dworak. The Design and Implementation of a Documentation Generator for the PRISM Language. In Proc. 4th International Conference on Dependability of Computer Systems (DepCoS-RELCOMEX'09), pages 91-98, IEEE Computer Society. June 2009. [bib] http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=5261015

2008

[ZHHW08] L. Zhang, H. Hermanns, E. M. Hahn and B. Wachter. Time-bounded model checking of infinite-state continuous-time Markov chains. In Proc. 8th International Conference on Application of Concurrency to System Design (ACSD'08), pages 98-107. 2008. [bib]

2007

[Der07] S. Derisavi. A Symbolic Algorithm for Optimal Markov Chain Lumping. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 139-154, Springer. March 2007. [bib] http://www.sce.carleton.ca/~derisavi/publications/index.html

2005

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

Case studies using PRISM (330)

2024

[TLE+24] Paul Tavolato, Robert Luh, Sebastian Eresheim, Simon Gmeiner and Sebastian Schrittwieser. Quantifying the Odds in Real World Attack Scenarios. In Proc. IEEE International Conference on Cyber Security and Resilience (IEEE-CSR'24). 2024. [Proposes an approach to modelling and analyse realistic cyber-attack scenarios, using PRISM for probability calculations.]
[JMT24] Kenneth Johnson, Samaneh Madanian and Catia Trubiani. Patterns of Applied Control for Public Health Measures on Transportation Services under Epidemic. In Proc. 19th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'24). 2024. [Proposes a methodology for modelling and analysing epidemic scenarios, using probabilistic model checking and PRISM.]
[RB24] Kaustabha Ray and Ansuman Banerjee. Autonomous Automotives on the Edge. In Proc. 37th International Conference on VLSI Design and 23rd International Conference on Embedded Systems (VLSID), pages 264-269, IEEE. 2024. [Proposes a probabilistic model checking approach to offloading automotive task processing to cloud/edge servers, using PRISM.]
[RRY+24] Maaike Van Roy, Pieter Robberechts, Wen-Chi Yang, Luc De Raedt and Jesse Davis. Leaving Goals on the Pitch: Evaluating Decision Making in Soccer. In MIT Sloan Sports Analytics Conference. 2024. [Analyses the success of decision making and strategies in football using probabilistic model checking and PRISM.]
[CMOF24] Mi Chen, Lynda Mokdad, Jalel Ben Othman and Jean-Michel Fourneau. Probabilistic performance evaluation of the class-A device in LoRaWAN protocol on the MAC layer. Performance Evaluation. 2024. [Uses probabilistic model checking and PRISM to analyse the performance of the LoRaWAN wireless network protocol. ]
[BHGB24] Abdelhakim Baouya, Brahim Hamid, Levent Gürgen and Saddek Bensalem. Rigorous Security Analysis of RabbitMQ Broker with Concurrent Stochastic Games. Internet of Things. 2024. [Performs a formal security analysis of the RabbitMQ broker using PRISM-games.]

2023

[CMOF23] Mi Chen, Lynda Mokdad, Jalel Ben Othman and Jean-Michel Fourneau. Probabilistic Model Checking for Unconfirmed Transmission in LoRaWAN on the MAC Layer. In Proc. IEEE Global Communications Conference (GLOBECOM'23). 2023. [Uses probabilistic model checking and PRISM to analyse the performance of the LoRaWAN wireless network protocol.]
[Ray23] Kaustabha Ray. Adaptive Service Placement for Multi-Access Edge Computing: A Formal Methods Approach. In Proc. IEEE International Conference on Web Services (ICWS'23). 2023. [Proposes a static-dynamic service placement policy for multi-access edge computing, making use of probabilistic model checking and PRISM.]
[ACSX23] Blair Archibald, Muffy Calder, Michele Sevegnani and Mengwei Xu. Quantitative Verification and Strategy Synthesis for BDI Agents. In Proc. NASA Formal Methods Symposium (NFM'23). 2023. [Uses PRISM to synthesise optimal strategies for probabilistic Belief-Desire-Intention agents.]
[WXLW23] Xia Wang, Yang Xu, Jun Liu and Keming Wang. Reliability analysis of mobile agent control system with multiple alternative plans. Soft Computing. 2023. [Studies the reliability of a mobile agent control system using PRISM.]
[WLM+23] Xia Wang, Jun Liu, Samuel Moore, Chris Nugent and Yang Xu. A Behavioural Hierarchical Analysis Framework in a Smart Home: Integrating HMM and Probabilistic Model Checking. Information Fusion. 2023. [Applies probabilistic model checking and PRISM to the analysis of smart home behavioural models.]
[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. ]
[RRY+23] Maaike Van Roy, Pieter Robberechts, Wen-Chi Yang, Luc De Raedt and Jesse Davis. A Markov Framework for Learning and Reasoning About Strategies in Professional Soccer. Journal of Artificial Intelligence Research (JAIR). 2023. [Proposes a technique to learn models of strategies in football and analyses them using probabilistic model checking.]

2022

[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.]
[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.]
[CRD+23] Jeroen Clijmans, Maaike Van Roy and Jesse Davis. Looking Beyond the Past: Analyzing the Intrinsic Playing Style of Soccer Teams. In Proc. Joint European Conference on Machine Learning and Knowledge Discovery in Databases (ECML/PKDD'22). 2022. [Models and analyses styles of play in football using probabilistic model checking and PRISM. ]
[TLE22] Paul Tavolato, Robert Luh and Sebastian Eresheim. Formalizing Real-world Threat Scenarios. In Proc. 8th International Conference on Information Systems Security and Privacy (ICISSP'22). 2022. [Uses PRISM-games to formalise attacker-defender scenarios for threat analysis.]
[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.]
[ELCP22] Mahmoud Elfar, Tung-Che Liang, Krishnendu Chakrabarty and Miroslav Pajic. Formal Synthesis of Adaptive Droplet Routing for MEDA Biochips. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 41(8), IEEE. 2022. [Presents a formal synthesis method for droplet routing in digital microfluidic biochips using PRISM-games.]
[GEM22] Saeedeh Sadat Sajjadi Ghaemmaghami, Seyedeh Sepideh Emam and James Miller. Automatically inferring user behavior models in large-scale web applications. Information and Software Technology. 2022. [Learns and analyses behavioural models of web users, with probabilistic models solved using PRISM.]

2021

[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[PBS21] Aisha Sattar Phulpoto, Sania Bhatti and Salahuddin Saddar. Probabilistic Modeling of Lossless Compression using Improved RLC Algorithm. International Journal of Computer Applications. 2021. [Uses PRISM to analyse a lossless compression algorithm called improved run-length coding (IRLC).]
[WMNA21] William Kavanagh, Alice Miller, Gethin Norman and Oana Andrei. Balancing Turn-Based Games With Chained Strategy Generation. IEEE Transactions on Games. 2021. [Proposes novel techniques for game balancing, building on probabilistic model checking and 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. ]
[AHG21] Mohammed N. Alharbi, Shihong Huang and David Garlan. A Probabilistic Model for Personality Trait Focused Explainability. In ECSA 2021 Companion Volume. 2021. [Proposes a framework for incorporating human personality traits models within automated decision-making, using PRISM and PRISM-games.]
[CGC+21] Maria Casimiro, David Garlan, Javier Cámara, Luís Rodrigues and Paolo Romano. A Probabilistic Model Checking Approach to Self-adapting Machine Learning Systems. In Proc. Software Engineering and Formal Methods (SEFM 2021) collocated workshops. 2021. [Presents a framework for machine-learning based self adaptation, instantiated using PRISM.]
[Wel21] Andrew Wells. Synthesis for Stochastic Robotic Systems. Ph.D. thesis, Rice University. 2021. [Proposes various synthesis techniques for robots in stochastic environments, using PRISM and PRISM-games.]
[ELCP21] Mahmoud Elfar, Tung-Che Liang, Krishnendu Chakrabarty and Miroslav Pajic. Formal Synthesis of Adaptive Droplet Routing for MEDA Biochips. In Proc. Design, Automation & Test in Europe Conference & Exhibition (DATE'21). 2021. [Presents a formal synthesis method for droplet routing in digital microfluidic biochips using PRISM-games.]
[CZZ21] Michael Cotner, Jixun Zhan and Zhen Zhang. A Computational Metabolic Model for Engineered Production of Resveratrol in Escherichia coli. ACS Synthetic Biology. 2021. [Proposes a probabilistic computational model for engineered production of Resveratrol in Escherichia coli, modelled in PRISM.]

2020

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

2019

[BBH+19] Nathalie Bertrand, Benjamin Bordais, Loïc Hélouët, Thomas Mari, Julie Parreaux and Ocan Sankur. Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking. In Proc. 3rd International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail'19), Springer. 2019. [Uses probabilistic model checking and PRISM to formally evaluate the performance of regulation algorithms in metro train lines.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[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.]
[ACMM19] Luca Arnaboldi, Ricardo M. Czekster, Charles Morisset and Roberto Metere. Modelling Load-Changing Attacks in Cyber-Physical Systems. In Proc. 10th International Workshop on the Practical Application of Stochastic Modelling (PASM'19). 2019. [Analyses load attacks on cyber-physical systems using probabilistic model checking and PRISM.]

2018

[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.]
[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.]
[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.]
[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.]
[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.]
[WBD+08] Matt Webster, Michael Breza, Clare Dixon, Michael Fisher and Julie McCann. Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks. In Proc. Automated Verification of Critical Systems 2018 (AVoCS'18) . 2018. [Verifies protocols for wireless sensor networks using probabilistic model checking and PRISM.]
[NF18] Mehran Alidoost Nia and Fathiyeh Faghih. Probabilistic Analysis of Self-Stabilizing Systems: A Case Study on a Mutual Exclusion Algorithm. In Proc. 2018 Real-Time and Embedded Systems and Technologies (RTEST'18), IEEE. 2018. [Uses PRISM to analyse and improve a mutual exclusion algorithm.]
[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.]
[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.]
[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. ]
[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.]
[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.]
[TMR18] Pedro J. Rivera Torres, E. I. Serrano Mercado and E. I. Serrano Mercado. Probabilistic Boolean Network Modeling of an Industrial Machine. Journal of Intelligent Manufacturing. 2018. [Uses Probabilistic Boolean Networks to model manufacturing processes, and analyses models using PRISM.]
[KML+18] Justus A. Kromer, Steffen Märcker, Steffen Lange, Christel Baier and Benjamin M. Friedrich. Decision making improves sperm chemotaxis in the presence of noise. Computational Biology, 14(4). 2018. [Uses probabilistic model checking and PRISM to study decision making in sperm chemotaxis.]
[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.]

2017

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

2016

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

2015

[HZHC15] Kangli He, Min Zhang, Jia He and Yixiang Chen. Probabilistic Model Checking of Pipe Protocol. In Proc. 9th International Symposium on Theoretical Aspects of Software Engineering (TASE'15). 2015. [Analyses the Pipe application layer protocol using probabilistic timed automata and PRISM.]
[Fra15] Joao Miguel Costa Sousa Franco. Automated Reliability Prediction and Analysis from Software Architectures. Ph.D. thesis, University of Coimbra. 2015. [Proposes automated techniques for predicting the reliability of software architectures, including the use of PRISM for model analysis.]
[CFR+15] Sanjian Chen, Lu Feng, Michael R. Rickels, Amy Peleckis, Oleg Sokolsky and Insup Lee. A Data-Driven Behavior Modeling and Analysis Framework for Diabetic Patients on Insulin Pumps. In Proc. IEEE International Conference on Healthcare Informatics (ICHI'15). 2015. [Proposes a modelling and analysis framework for the usage of insulin pumps, and studies the resulting models using PRISM.]
[UC15] Jose Ignacio Aizpurua Unanue and Victoria M. Catterson. On the use of probabilistic model-checking for the verification of prognostics applications. In Proc. IEEE Seventh International Conference on Intelligent Computing and Information Systems (ICICIS'15). 2015. [Applies probabilistic model checking and PRISM to prognostic techniques aimed at estimating the remaining useful life of assets.]
[CCDR15] Giuseppe Cicotti, Luigi Coppolino, Salvatore D'Antonio and Luigi Romano. Runtime Model Checking for SLA Compliance Monitoring and QoS Prediction. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, 6(2). 2015. [Proposes a QoS prediction approach using PRISM and applied to a smart grid case study.]
[CC15] Giuseppe Cicotti and Antonio Coronato. Towards a Probabilistic Model Checking-based approach for Medical Device Risk Assessment. In Proc. IEEE International Workshop on Medical Measurement and Applications (MEMEA'15). 2015. [Uses probabilistic model checking and PRISM in a new approach for quantitative medical device risk assessment.]
[TMR15] Pedro J. Rivera-Torres, E.I. Serrano Mercado and Anido L. Rifon. Probabilistic Boolean network modeling and model checking as an approach for DFMEA for manufacturing systems. Journal of Intelligent Manufacturing, pages 1-21, Springer. 2015. [Uses probabilistic Boolean networks and PRISM to analyse automated manufacturing assembly processes.]
[ZWC+15] Conghua Zhou, Yong Wang, Meiling Cao, Jianqi Shi and Yang Liu. Formal Analysis of MAC in IEEE 802.11p with Probabilistic Model Checking. In Proc. International Symposium on Theoretical Aspects of Software Engineering (TASE'15), pages 55-62, IEEE. 2015. [Uses probabilistic model checking and PRISM to analyse 802.11p for vehicular ad-hoc networks.]
[RMT15] Arunkumar Ramaswamy, Bruno Monsuez and Adriana Tapus. Model-driven self-adaptation of robotics software using probabilistic approach. In Proc. 2015 European Conference on Mobile Robots (ECMR'15). 2015. [Uses PRISM as part of a framework for model-driven self-adaptation of robotics software.]
[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.]
[RGH15] Daniël Reijsbergen, Stephen Gilmore and Jane Hillston. Patch-based Modelling of City-centre Bus Movement with Phase-type Distributions. In Proc. 7th International Workshop on Practical Applications of Stochastic Modelling (PASM'14), volume 310 of ENTCS, pages 157-177. 2015. [Uses HyperStar and PRISM on a stochastic performance model of a public transportation network.]
[CMG15] Javier Cámara, Gabriel A. Moreno and David Garlan. Reasoning about Human Participation in Self-Adaptive Systems. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes a formal framework for reasoning about human involvement in self-adaptive systems, using PRISM-games as an underlying model checker.]
[ASBL+15] A. Aldini, J.-M. Seigneur, C. Ballester Lafuente, X. Titi and J. Guislain. Formal Modeling and Verification of Opportunity-enabled Risk Management. In Proc. Trustcom International Symposium on Recent Advances of Trust, IEEE. 2015. [Formally analyses the opportunity-enabled risk management (OPPRIM) security framework using probabilistic model checking and PRISM.]
[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.]
[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.]
[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.]
[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. ]
[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.]
[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.]
[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.]

2014

[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]
[SCG+14] Bradley Schmerl, Javier Cámara, Jeffrey Gennari, David Garlan, Paulo Casanova, Gabriel A. Moreno, Thomas J. Glazier and Jeffrey M. Barnes. Architecture-based self-protection: composing and reasoning about denial-of-service mitigations. In Proc. 2014 Symposium and Bootcamp on the Science of Security (HotSoS'14). 2014. [Proposes adaptive techniques for denial-of-service mitigation, including formal analysis of adaptation strategies using PRISM.]
[FYO14] Ling Fang, Yoriyuki Yamagata and Yutaka Oiwa. Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking. In Proc. 3rd International Workshop on Engineering Safety and Security Systems 2014 (ESSS'14), volume 150 of EPTCS, pages 35-49. 2014. [Uses probabilistic model checking and PRISM to analyse resilience strategies for micro processor units.]
[ZR14] Yang Zhao and Kristin Yvonne Rozier. Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems. In Proc. IEEE/ACM 2014 International Conference on Computer-Aided Design (ICCAD'14), IEEE/ACM. 2014. [bib] [Uses probabilistic model checking and PRISM to study safety properties of automated air traffic control systems.]
[Ald14] Alessandro Aldini. Saving Privacy in Trust-Based User-Centric Distributed Systems. In Proc. 8th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE'14), pages 76-81. 2014. [Analyses privacy, cost and trust trade-offs in user-centric distributed systems using PRISM.]
[SBN14] Pravati Swain, Purandar Bhaduri and Sukumar Nandi. Probabilistic model checking of IEEE 802.11 IBSS power save mode. International Journal of Wireless and Mobile Computing, 7(7), pages 465-474. 2014. [Uses probabilistic model checking and PRISM to analyse a power management algorithm for Independent Basic Service Set (IBSS) from the IEEE 802.11 standard for wireless local area networks.]
[CMG14] Javier Cámara, Gabriel A. Moreno and David Garlan. Stochastic Game Analysis and Latency Awareness for Proactive Self-Adaptation. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), pages 155-164, ACM. 2014. [Uses PRISM-games to analyse adaptation tactic latency in self-adaptive systems.]
[BCG14] Ludovica Luisa Vissat, Allan Clark and Stephen Gilmore. Finding optimal timetables for Edinburgh bus routes. In Proc. 7th International Workshop on Practical Applications of Stochastic Modelling (PASM'14). 2014. [Uses various techniques and tools, including PRISM, to analyse and optimise bus reliability.]
[SBWA14] Khalid Sultan, Jamal Bentahar, Wei Wan and Faisal Al-Saqqar. Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments. Expert Systems with Applications, 41(14), pages 6291-6304, Elsevier. 2014. [Proposes techniques for analysing probabilistic multi-agent systems, implemented using PRISM.]
[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.]
[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.]
[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.]
[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.]
[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.]

2013

[PLM+13] Zhaoguang Peng, Yu Lu, Alice Miller, Chris Johnson and Tingdi Zhao. A Probabilistic Model Checking Approach to Analysing Reliability, Availability, and Maintainability of a Single Satellite System. In Proc. 7th European Symposium on Computer Modelling and Simulation (EMS'13), pages 611-616. 2013. [Uses probabilistic model checking and PRISM to analyse reliability, availability and maintainability properties of a satellite system.]
[KV13] Jayanand Asok Kumar and Shobha Vasudevan. Formal Probabilistic Timing Verification in RTL. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(5), pages 788-801, IEEE. 2013. [Analyses timing properties of RTL designs, using the SHARPE tool and a connection to PRISM.]
[JKG13] Benjamin Johnson and Hadas Kress-Gazit. Analyzing and revising high-level robot behaviors under actuator error. In Proc. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'13), pages 741-748. 2013.
[GMZ13] H. Gao, H. Miao and H. Zeng. Predictive web service monitoring using probabilistic model checking. International Journal on Applied Mathematics & Information Sciences, 6(1L), pages 139–148. 2013. [Uses probabilistic model checking and PRISM to predict web service reliability.]
[RSLG13] Mikołaj Rybiński, Zuzanna Szymańska, Sławomir Lasota and Anna Gambin. Modelling the efficacy of hyperthermia treatment. J. R. Soc. Interface, 10(88). 2013. [Analyses models of the effectiveness of hyperthermia in the context of a heat-shock response mechanism, using ODEs and PRISM.]
[BEK+13] Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Selec. In Proc. NASA Formal Methods Symposium (NFM'13), pages 307-321. 2013. [Verifies the Probabilistic-Write/Copy-Select (PWCS) protocol using PRISM.]
[CG13] Sagar Chaki and Joseph Andrew Giampapa. Probabilistic Verification of Coordinated Multi-robot Missions. In Proc. 20th International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 135-153, Springer. 2013. [Proposes techniques to verify multi-robot systems, including the use of PRISM.]
[KATH13] Adil Khurram, Haider Ali, Arham Tariq and Osman Hasan. Formal Reliability Analysis of Protective Relays in Power Distribution Systems. In Proc. International Workshop on Formal Methods for Industrial Critical Systems (FMICS'13), pages 169-183, Springer. 2013. [Models and verifies power distribution relays using PRISM.]
[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.]
[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.]
[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.]
[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.]

2012

[BMJM12] S. Bhatti, S. Memon, I.A. Jokhio and M.A. Memon. Modelling and symmetry reduction of a target-tracking protocol using wireless sensor networks. IET Communications, 6(10), pages 1205-1211. 2012.
[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.]
[KDF12] Savas Konur, Clare Dixon and Michael Fisher. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems, 60(2), pages 199-213. 2012. [bib] [Uses probabilistic model checking and PRISM to analyse the effectiveness of robot swarms.]
[LLL+12] Robyn Lutz, Jack Lutz, James Lathrop, Titus Klinge, Eric Henderson, Divita Mathur and Dalia Abo Sheasha. Engineering and Verifying Requirements for Programmable Self-Assembling Nanomachines. In Proc. 34th ACM/IEEE International Conference on Software Engineering (ICSE'12). 2012. [bib] [Proposes validation techniques for programmable DNA self-assemblies, using DNA origami pliers as an example, and applying PRISM for analysis.]
[AB12] Alessandro Aldini and Alessandro Bogliolo. Model Checking of Trust-Based User-Centric Cooperative Networks. In Proc. 4th International Conference on Advances in Future Internet (AFIN'12). 2012.
[LSPM12] Qian Li, Peter Schaffer, Jun Pang and Sjouke Mauw. Comparative Analysis of Clustering Protocols with Probabilistic Model Checking. In Proc. 6th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'12). 2012.
[BPBD12] Manuele Brambilla, Carlo Pinciroli, Mauro Birattari and Marco Dorigo. Property-driven Design for Swarm Robotics. In Proc. 11th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'12). 2012. [Uses probabilistic model checking and PRISM as part of a design process for swarm robotics.]
[HYF+12] Kang He, Hongli Yang, Yachao Feng, Yuan Liu and Zongyan Qiu. Performance Analysis of Data Gathering Protocol Using PRISM. In Proc. 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'12), pages 96-105. 2012. [Uses PRISM to analyse the Power Efficient Algorithm for Data Gathering (PEADG) protocol.]
[OJMD12] Samir Ouchani, Yosr Jarraya, Otmane Ait Mohamed and Mourad Debbabi. Probabilistic Attack Scenarios to Evaluate Policies over Communication Protocols. Journal of Software, 7(7), pages 1488-1495. 2012. [Analyses communication protocol attack scenarios with PRISM, using RTSP/SRTP as an example.]
[LJL+12] Lixing Li, Zhi Jin, Ge Li, Liwei Zheng and Qiang Wei . Modeling and Analyzing the Reliability and Cost of Service Composition in the IoT: A Probabilistic Approach. In Proc. 19th IEEE International Conference on Web Services (ICWS'12), pages 584-591 . 2012. [Uses PRISM to analyse compositions of web services.]
[PB12] Sophia Petridou and Stylianos Basagiannis. Towards Energy Consumption Evaluation of the SSL Handshake Protocol in Mobile Communications. In Proc. 9th IEEE Annual Conference on Wireless on-demand Networks Systems and Services (IEEE WONS'12). 2012. [Analyses the energy consumption of the SSL handshake protocol using a PRISM CTMC model.]
[AC12] Oana Andrei and Muffy Calder. Trend-Based Analysis of a Population Model of the AKAP Scaffold Protein. Transactions on Computational Systems Biology, XIV, pages 1-25, Springer. 2012. [Studies the AKAP scaffold protein by introducing a notion of stochastic trends and using PRISM for model analysis.]
[BBOM12] Paolo Ballarini, Jalel Ben-Othman and Lynda Mokdad. Quantitative Verification of WiMAX Traffic Shaping Solutions. In Proc. 7th International Symposium on Intelligent System Techniques for Ad hoc and Wireless Sensor Networks (IST-AWSN). 2012. [Uses probabilistic model checking and PRISM to analyse traffic-shaping schemes for the IEEE 802.16 (WiMAX) standard.]
[SSK+12] Emmanouela Stachtiari, Yannis Soupionis, Panagiotis Katsaros, Anakreontas Mentis and Dimitris Gritzalis. Probabilistic model checking of CAPTCHA admission control for DoS resistant anti-SPIT protection. In Proc. 7th International Conference on Critical Information Infrastructures Security (CRITIS'12). 2012. [Studies the effectiveness of admission control policies for DoS-resistanct CAPTCHA schemes using probabilistic model checking and PRISM.]
[YTP+12] Qixia Yuan, Panuwat Trairatphisan, Jun Pang, Sjouke Mauw, Monique Wiesinger and Thomas Sauter. Probabilistic Model Checking of the PDGF Signaling Pathway. Transactions on Computational Systems Biology, XIV, pages 151-180. 2012. [Analyses the PDGF signalling pathway using PRISM.]
[LR12] Adalberto Llarena and David Rosenblueth. Model Checking Applied to Humanoid Robotic Soccer. In Advances in Autonomous Robotics, volume 7429 of LNCS, Springer. 2012. [Uses PRISM to synthesise parameters of probabilistic strategies for humanoid robotic football.]
[CCN12] Luca Cardelli and Attila Csikász-Nagy. The Cell Cycle Switch Computes Approximate Majority. Nature Scientific Reports, 2. 2012. [Studies the cell cycle switch as a computing device, based on deterministic/stochastic simulation and probabilistic verification with PRISM.]
[TTL12] Anton Tarasyuk, Elena Troubitsyna and Linas Laibinis. Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In Proc. 9th International Conference on Integrated Formal Methods (IFM'12), pages 237-252. 2012. [Uses PRISM to analyse dynamic service architectures modelled in a probabilistic extension of Event-B.]
[KH12] K. Kobayashi and K. Hiraishi. Symbolic approach to verification and control of deterministic/probabilistic Boolean networks. IET Systems Biology, 6(6), pages 215-222. 2012. [bib] [Applies PRISM to the analysis of probabilistic Boolean networks, using an apoptosis network and a WNT5A network as examples.]
[CKJ12] Radu Calinescu, Shinji Kikuchi and Kenneth Johnson. Compositional Reverification of Probabilistic Safety Properties for Large-Scale Complex IT Systems. In Proc. 17th Monterey Workshop on Development, Operation and Management of Large-Scale Complex IT Systems. 2012. [Uses PRISM and its compositional (assume-guarantee) extensions to analyse large-scale complex IT systems (LSCITS).]
[LLL+12b] Robyn Lutz, Jack Lutz, James Lathrop, Titus Klinge, Divita Mathur, D. M. Stull, Taylor Bergquist and Eric Henderson. Requirements Analysis for a Product Family of DNA Nanodevices. In Proc. 20th IEEE International Requirements Engineering Conference. 2012. [Applies requirements engineering methods to DNA nanodevices and uses PRISM to verify the generated properties.]
[AASB12] Zaid Al-bayati, O. Ait Mohamed, Yvon Savaria and Mounir Boukadoum. Probabilistic model checking of clock domain crossing interfaces. In Proc. IEEE 10th International New Circuits and Systems Conference (NEWCAS'12). 2012. [Uses PRISM to verify clock domain crossing (CDC) protocols.]
[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.]
[HDS12] Brendan Hall, Kevin Driscoll and Kevin Schweike. Verification and validation of distributed flight critical systems. In Proc. IEEE/AIAA 31st Digital Avionics Systems Conference (DASC'12). 2012. [Summarises Honeywell's work on a program for verification and validation of flight critical systems, including using PRISM to evaluate fault-tolerant protocols.]

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]
[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]
[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
[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]
[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]
[TK11] Li Tan and Axel Krings. An Adaptive N-variant Software Architecture for Multi-Core Platforms: Models and Performance Analysis. In Proc. International Conference on Computational Science and Its Applications, Part II (ICCSA'11), pages 490-505. 2011. [bib]
[CDGFS11] J. Clement, C. Delporte-Gallet, H. Fauconnie and M. Sighireanu. Guidelines for the Verification of Population Protocols. In Proc. 31st International Conference on Distributed Computing Systems (ICDCS'11). 2011. [bib]
[DKBS11] Tushar Deshpande, Panagiotis Katsaros, Stylianos Basagiannis and Scott Smolka. Formal Analysis of the DNS Bandwidth Amplification Attack and Its Countermeasures Using Probabilistic Model Checking. In Proc. 13th IEEE International Symposium on High-Assurance Systems Engineering (HASE'11), pages 360-367. 2011. [bib]
[MZ11] Ravie C. Muniyandi and Abdullah M. Zin. Membrane Computing as a Modeling Tool for Discrete Systems. Journal of Computer Science, 7(11), pages 1667-1673. 2011. [bib]
[MZ11b] Ravie C. Muniyandi and Abdullah M. Zin. Evaluating Ligand-Receptor Networks of TGF-β with Membrane Computing. Pakistan Journal of Biological Sciences, 14, pages 1100-1108. 2011. [bib]
[MST11a] Tamara Mendt, Carsten Sinz and Olga Tveretina. Probabilistic Model Checking of Constraints in a Supply Chain Business Process. In Business Information Systems, volume 87 of Lecture Notes in Business Information Processing, pages 1-12. 2011.
[NIOK11] T. Nagaoka and A. Ito and K. Okano and S. Kusumoto. QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation. IEICE Transactions on Information and Systems, E94.D(5), pages 958-966 . 2011.
[Dut11] Bruno Dutertre. Probabilistic Analysis of Distributed Fault-Tolerant Systems. Technical report CR–2011-217090, NASA. 2011. http://ntrs.nasa.gov/search.jsp?R=20110011564
[KF11] Savas Konur and Michael Fisher. Formal Analysis of a VANET Congestion Control Protocol through Probabilistic Verification. In Proc. 73rd IEEE Vehicular Technology Conference (VTC'11). 2011.
[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.]
[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] [Describes work by Fujitsu researchers using PRISM to optimise live migration of virtual machines in the cloud.]

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.
[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/
[KV10] J. A. Kumar and S. Vasudevan. Statistical guarantees of performance for MIMO designs. In Proc. IEEE/IFIP International Conference on Dependable Systems & Networks (DSN'10). 2010. [bib]
[KV10b] J. A. Kumar and S. Vasudevan. Automatic compositional reasoning for probabilistic model checking of hardware designs. In Proc. 7th International Conference on Quantitative Evaluation of SysTems (QEST'10), IEEE CS Press. 2010. [bib]
[STK+10] D. Schumm, O. Turetken, N. Kokash, A. Elgammal, F. Leymann and W.-J. van den Heuvel. Business Process Compliance through Reusable Units of Compliant Processes. In Proc. 10th International Conference on Current Trends in Web Engineering (ICWE'10). 2010. [bib]
[KH10] K. Kobayashi and K. Hiraishi. Reachability analysis of probabilistic Boolean networks using model checking. In Proc. SICE Annual Conference 2010, pages 829-832. 2010. [bib]
[RAFL10] G. N. Rodrigues, V. Alves, R. Franklin and L. Laranjeira. Dependability Analysis in the Ambient Assisted Living Domain: an Exploratory Case Study. In Proc. 4th Brazilian Symposium on Software Components, Architectures and Reuse, pages 150-159. 2010. [bib]
[YZH+10] Hongli Yang, Liang Zhou, Kang He, Chen Deng, Xiangpeng Zhao and Zongyan Qiu. A probabilistic QoS model-checking for dynamic routing protocol. In Proc. 10th International Conference on Quality Software (QSIC'10), pages 441-448, IEEE. 2010. [bib]
[OGS10] P. Oliveira, R. Gomes and M. Song. Large Scale Genetic Identity Inference Using Probabilistic Model Checking. In 2010 IEEE International Conference on Systems Man and Cybernetics (SMC'10), pages 3508-3512, IEEE. 2010. [bib]
[KSB10] Heiko Koziolek, Bastian Schlich and Carlos Bilich. A Large-Scale Industrial Case Study on Architecture-based Software Reliability Analysis. In Proc. IEEE 21st International Symposium on Software Reliability Engineering (ISSRE'10), pages 279-288. 2010. [bib]
[HWHY10] Wei Huang, Gengyu Wei, Nan Hu and Yixian Yang. Design and Analysis of Heartbeat Protocol in NIDS Cluster. In Proc. 2nd International Conference on Future Computer and Communication (ICFCC'10). 2010.
[KDF10] Savas Konur, Clare Dixon and Michael Fisher. Formal Verification of Probabilistic Swarm Behaviours. In Proc. 7th International Conference on Swarm Intelligence (ANTS'10), volume 6234 of LNCS, pages 440-447, Springer. 2010. [bib]
[BMA10] Cristiano Bertolini, Alexandre Mota and Eduardo Aranha. Calibrating Probabilistic GUI Testing Models Based on Experiments and Survival Analysis. In Proc. 21st IEEE International Symposium on Software Reliability Engineering (ISSRE'10), pages 319-328. 2010. [Uses PRISM to evaluate software testing techniques for graphical user interfaces.]
[GMS+10] Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe Ferri and Julio Buzzi. Systematic Model-Based Safety Assessment Via Probabilistic Model Checking. In 4th International Symposium on Leveraging Applications on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'10), pages 625-639, Springer. 2010. [Uses PRISM for quantitative safety assessment, with a case study of an actuator control system.]
[YK10] Haidi Yue and Joost-Pieter Katoen. Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption. In Proc. 17th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA'10) , volume 6148 of LNCS, pages 247–261, Springer. 2010. [Analyses a randomised leader election protocol using PRISM.]
[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]

2009

[MKUM09] Paulo Maia, Jeff Kramer, Sebastián Uchitel and Nabor Mendonça. Towards accurate probabilistic models using state refinement. In Proc. 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/SIGSOFT FSE'09), pages 281-284. 2009. [Presents state refinement techniques for generating accurate probabilistic models which are analysed using PRISM.]
[BKPA09] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. Probabilistic model checking for the quantification of DoS security threats. Computers & Security, Elsevier. 2009. [bib]
[BMM09] Paolo Ballarini, Radu Mardare and Ivan Mura. Analysing Biochemical Oscillation through Probabilistic Model Checking. In Proc. 2nd Workshop From Biology to Concurrency and Back (FBTC'08), volume 229 (issue 1) of Electronic Notes in Theoretical Computer Science, pages 3-19, Elsevier. 2009. [bib]
[CGHV09] M. Calder, S. Gilmore, J. Hillston and V. Vyshemirsky. Formal methods for biochemical signalling pathways. In Formal Methods: State of the Art and New Directions, Springer. To appear. 2009. [bib]
[BW09] B. Beckert and M. Wagner. Probabilistic Models for the Verification of Human-Computer Interaction. In Proc. 32nd Annual German Conference on Artificial Intelligence. 2009. [bib]
[BGK+09] T. Berczes, G. Guta, G. Kusper, W. Schreiner and J. Sztrik. Analyzing a Proxy Cache Server Performance Model with the Probabilistic Model Checker PRISM. In Proc. 5th International Workshop on Automated Specification and Verification of Web Systems (WWV'09). 2009. [bib]
[AFG+09] H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner and S. Leue. Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). 2009. [bib]
[BF09] R. Bakhshi and A. Fehnker. On the impact of modelling choices for distributed information spread. A comparative study. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). 2009. [bib]
[MS09] J. Misra and I. Saha. A Reinforcement Model for Collaborative Security and Its Formal Analysis. In Proc. New Security Paradigms Workshop (NSPW'09). 2009. [bib] [Proposes a reinforcement framework for collaborative monitoring of security violations and anlayses it using PRISM.]
[SM09] I. Saha and D. Mukhopadhyay. Quantitative Analysis of a Probabilistic Non-repudiation Protocol through Model Checking. In Proc. 5th International Conference on Information Systems Security (ICISS'09), volume 5905 of LNCS, pages 292-300, Springer. 2009. [bib]
[DTC+09] A. Dhama, O. Theel, P. Crouzen, H. Hermanns, R. Wimmer and B. Becker. Dependability Engineering of Silent Self-stabilizing Systems. In Proc. 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems, volume 5873 of LNCS, pages 238-253, Springer. 2009. [bib]
[CV09] M. Casadei and M. Viroli. Using probabilistic model checking and simulation for designing self-organizing systems. In Proc. ACM Symposium on Applied Computing (SAC'2009), pages 2103-2104. 2009. [bib]
[JM09] L. Jagadeesan and V. Mendiratta. Voice Communication Mashups: Formal Specification and Composition of Service Level Agreements. In 3rd International Conference on Next Generation Mobile Applications, Services and Technologies (NGMAST'09). 2009. [bib]
[STTK09] Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Koichi Takahashi and Tohru Kikuno. Probabilistic Model Checking of the One-Dimensional Ising Model. IEICE Transactions on Information and Systems, E92.D(5), pages 1003-1011. 2009. [bib]
[Wer09] Frank Werner. Applied Formal Methods in Wireless Sensor Networks. Ph.D. thesis, University of Karlsruhe. 2009.
[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.]
[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]

2008

[Tan08] Li Tan. Model check stochastic supply chains. In Proc. IEEE International Conference on Information Reuse and Integration (IRI'08), pages 416 - 421. 2008.
[BKPA08] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. A Probabilistic Attacker Model for Quantitative Verification of DoS Security Threats. In Proc. 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'08), pages 12-19, IEEE CS Press. 2008. [bib] http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=4591503&arnumber=4591526&count=285&index=22
[CT08] A. Coker and V. Taylor. Performance and Reliability Analysis of a Scaled Multi-Switch Junction Crossbar Nanomemory and Demultiplexer. In Proc. IEEE NANO Conference. 2008. [bib] http://prophesy.cs.tamu.edu/publications.html
[WS08] F. Werner and P. Schmitt. Analysis of the Authenticated Query Flooding Protocol by Probabilistic Means. In Proc. 5th Annual Conference on Wireless On demand Network Systems and Services (WONS'08), pages 101-104. 2008. [bib] http://ieeexplore.ieee.org/xpl/tocresult.jsp?isnumber=4459341&isYear=2008
[BPdV08] D. Bosnacki, T. Pronk and E. de Vink. In Silico Modelling and Analysis of Ribosome Kinetics and aa-tRNA Competition. In R.-J. Back and I. Petre (editors), Proc. Workshop on Computational Models for Cell Processes (COMPMOD'08), pages 23-38. 2008. [bib] http://www.win.tue.nl/~evink/research/publications.html
[SAA+08] A. Susu, A. Acquaviva, A. Atienza and and A. De Micheli. Stochastic Modeling and Analysis for Environmentally Powered Wireless Sensor Nodes. In Proc. 6th International Symposium on Modeling and Optimization in Mobile, Ad Hoc, and Wireless Networks (WiOPT'08), pages 11-20. 2008. [bib] http://lsi.epfl.ch/page13139.html
[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
[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]
[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]
[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
[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

2007

[HVH07] Tran Thi Bich Hanh and Dang Van Hung. Verification of an Air-Traffic Control System with Probabilistic Real-time Model-checking. Technical report , UNU-IIST United Nations University International Institute for Software Technology. 2007. [bib]
[HBGS07] F. He, L. Baresi, C. Ghezzi and P. Spoletini. Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata. In Proc. Formal Techniques for Networked and Distributed Systems (FORTE'07), volume 4574 of Lecture Notes in Computer Science, pages 247-262, Springer. 2007. [bib] http://www.springerlink.com/content/h0438p764643727u/
[Kal07] E. Kaldeli. Investigating formal representations of PIN block attacks. Masters thesis, School of Informatics, University of Edinburgh. 2007. [bib] http://www.inf.ed.ac.uk/publications/thesis/online/IM070467.pdf
[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]
[STKT07] Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno and Koichi Takahashi. Analyzing the One Dimensional Ising Model by Probabilistic Model Checking. In Proc. IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007). October 2007.
[LJ07] C. Langmead and S. Jha. Predicting Protein Folding Kinetics Via Temporal Logic Model Checking. In 7th International Workshop on Algorithms in Bioinformatics (WABI'07), volume 4645 of Lecture Notes in Computer Science, pages 252-264, Springer. September 2007. [bib]
[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/
[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]
[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/
[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
[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
[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
[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

2006

[Ste06] G. Steel. Formal Analysis of PIN Block Attacks. Theoretical Computer Science, 367(1-2), pages 257-270, Elsevier. 2006. [bib]
[CVGO06] M. Calder, V. Vyshemirsky, D. Gilbert and R. Orton. Analysis of signalling pathways using continuous time Markov chains. Transactions on Computational Systems Biology VI, 4220, pages 44-67, Springer. 2006. [bib] http://www.dcs.gla.ac.uk/~muffy/papers.html
[Che06] L. Cheung. Reconciling Nondeterministic and Probabilistic Choices. Ph.D. thesis, Radboud University of Nijmegen. 2006. [bib] http://theory.csail.mit.edu/~lcheung/
[FG06] A. Fehnker and P. Gao. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In Proc. 5th International Conference on Ad-Hoc, Mobile, and Wireless Networks (ADHOC-NOW'06), volume 4104 of LNCS, pages 128-141, Springer. 2006. [bib] http://www.cse.unsw.edu.au/~ansgar/
[CB06] D. Chu and I. Blomfield. Orientational control is an efficient control mechanism for phase switching in the E.coli fim system. Journal of Theoretical Biology, Elsevier. To appear. 2006. [bib] http://www.cs.kent.ac.uk/people/staff/dfc/site/
[BSGG06] D. Bhaduri, S. Shukla, P. Graham and M. Gokhale. Comparing Reliability-Redundancy Trade-offs for Two Von Neumann Multiplexing Architectures. IEEE Transactions on Nanotechnology. To appear. 2006. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html
[BFW06b] Paolo Ballarini, Michael Fisher and Michael Wooldridge. Uncertain Agent Verification through Probabilistic Model-Checking. In Proc. 3rd International Workshop on Safety and Security in Multi-agent Systems (SASEMAS'06). 2006. [bib]
[MF06] Annabelle McIver and Ansgar Fehnker. Formal Techniques for the Analysis of Wireless Networks. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'06), pages 263–270. 2006. [Applies various formal verification techniques to wireless networks, including probabilistic model checking with PRISM.]
[BM06] Paolo Ballarini and Alice Miller. Model Checking Medium Access Control for Sensor Networks. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods (ISoLA'06), pages 255-262. 2006. [Uses PRISM to verify S-MAC, a medium access control protocol for wireless sensor networks.]
[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
[GF06c] J. Greifeneder and J. Frey. Optimizing Quality of Control in Networked Automation Systems using Probabilistic Models. In Proc. 11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'06), pages 372-379. September 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GF06d] J. Greifeneder and J. Frey. Probabilistic Hybrid Automata with Variable Step Width Applied to the Analysis of Networked Automation Systems. In Proc. 3rd IFAC Workshop on Discrete Event System Design (DESDes'06), pages 283-288. September 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GF06b] J. Greifeneder and G. Frey. Determination of Delay Times in Failure Afflicted Networked Automation Systems using Probabilistic Model Checking. In Proc. 6th IEEE International Workshop on Factory Communication Systems (WFCS'06), pages 263-272. June 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GF06] J. Greifeneder and G. Frey. Dependability analysis of networked automation systems by probabilistic delay time analysis. In Proc. 12th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'06), pages 269-274. May 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[ZH06] M. Zhang and D. Van Hung. Formal Analysis of Streaming Downloading Protocol for System Upgrading. In Proc. 4th Workshop on Quantitative Aspects of Programming Languages (QAPL 06). Also available as UNU-IIST Report No. 332. April 2006. [bib] http://www.iist.unu.edu/~dvh/publications_2.html
[BCS+06] D. Bhaduri, S. Shukla, D. Coker, V. Taylor, P. Graham and M. Gokhale. A Hybrid Framework for Design and Analysis of Fault Tolerant Architectures and its Applications to Nanoscale Molecular Crossbar Memories. In Proc. Design, Automation and Test in Europe (DATE'06). March 2006. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html
[BFW06] Paolo Ballarini, Michael Fisher and Michael Wooldridge. Automated Game Analysis via Probabilistic Model Checking: A Case Study. In Proc. 3rd Workshop on Model Checking and Artificial Intelligence (MoChArt'05), volume 149 of ENTCS, pages 125-137, Elsevier. February 2006. [bib] http://www.csc.liv.ac.uk/~mjw/pubs/

2005

[GB05] N. Geisweiller and J. Bonte. Performance Evaluation of a Real-time Simulation Architecture using Probabilistic Model Checking. In Proc. Workshop on Structural Operational Semantics (SOS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 3-24. 2005. [bib] http://linkinghub.elsevier.com/retrieve/pii/S1571066105001854
[Che05] L. Cheung. Randomized Wait-Free Consensus using An Atomicity Assumption. In Proc. 9th International Conference on Principles of Distributed Systems (OPODIS'05). Full version available as Technical Report ICIS-R05035, Institute for Computing and Information Sciences, Radboud University Nijmegen. November 2005. [bib] http://theory.csail.mit.edu/~lcheung/
[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/
[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
[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
[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
[RG05] A. Roy and K. Gopinath. Improved Probabilistic Models for 802.11 Protocol Verification. In Proc. 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 239-252, Springer-Verlag. July 2005. [bib]
[BML05b] M. ter Beek, M. Massink and D. Latella. Towards Model Checking Stochastic Aspects of the thinkteam User Interface. In M. Harrison (editor), Proc. 12th International Workshop on Design, Specification and Verification of Interactive Systems (DSVIS'05), volume 3941 of Lecture Notes in Computer Science, pages 39-50, Springer. July 2005. [bib] http://fmt.isti.cnr.it/~mtbeek/
[CKKP05] L. Cloth, J.-P. Katoen, M. Khattri and R. Pulungan. Model checking Markov reward models with impulse rewards. In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 722-731, IEEE CS Press. June 2005. [bib]
[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
[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
[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
[NPBG05] R. Nagarajan, N. Papanikolaou, G. Bowen and S. Gay. An Automated Analysis of the Security of Quantum Key Distribution. In Proc. 3rd International Workshop on Security Issues in Concurrency (SecCo'05). 2005. [bib] http://www.dcs.warwick.ac.uk/~nikos/
[CVGO05] M. Calder, V. Vyshemirsky, D. Gilbert and R. Orton. Analysis of signalling pathways using the PRISM model checker. In Proc. Computational Methods in Systems Biology (CMSB'05), pages 179-190. 2005. [bib] http://www.dcs.gla.ac.uk/~muffy/papers.html
[BML05a] M. ter Beek, M. Massink, and D. Latella. Towards Model Checking Stochastic Aspects of the thinkteam User Interface - FULL VERSION. Technical report 2005-TR-18, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche. 2005. [bib] http://fmt.isti.cnr.it/WEBPAPER/TRdsvis.pdf

2004

[Shm04] V. Shmatikov. Probabilistic Model Checking of an Anonymity System. Journal of Computer Security, 12(3/4), pages 355-377. 2004. [bib] http://www.cs.utexas.edu/~shmat/index.html
[FP04] W. Fokkink and J. Pang. Simplifying Itai-Rodeh leader election for anonymous rings. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 53-68, Elsevier Science. September 2004. [bib] http://www.lix.polytechnique.fr/~pangjun/research/pub.html
[DSS04] R. Dingledine, V. Shmatikov and P. Syverson. Synchronous Batching: From Cascades to Free Routes. In Proc. 4th Workshop on Privacy Enhancing Technologies (PET). May 2004. [bib] http://www.csl.sri.com/users/shmat/
[BS04] D. Bhaduri and S. Shukla. NANOPRISM: A Tool for Evaluating Granularity vs. Reliability Trade-offs in Nano Architectures. In Proc. 14th Great Lakes Symposium on VLSI (GLSVLSI'04), ACM. April 2004. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html#Recent Publications
[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/
[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

2002

[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

Others (1)

2024

[KM24] Aka Sai Lalith Kumar and Sweta Mishra. Ransomware Criminal Smart Contract. In Proc. IEEE International Conference on Blockchain (Blockchain'24). 2024. [Proposes and evaluates, using PRISM, a protocol for criminal smart contracts.]

Sort by: date, type, title, subject

PRISM Bibliography (external)

Tool/language connections to PRISM (238)

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Extensions and adaptions to PRISM (63)

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2013

2012

2011

2010

2009

2008

2007

2005

Case studies using PRISM (330)

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2002

Others (1)

2024

Publications