www.prismmodelchecker.org

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.

458 publications:

Book chapters

2009

Journal papers

2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003

Conference papers

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.]
  • [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. [Develops a solving lexicographic reachability-safety objectives on stochastic games, implemented as an extension of PRISM-games.]
  • [MACD20] Nabor C. Mendonça, Carlos Mendes Aderaldo, Javier Cámara and David Garlan. Model-Based Analysis of Microservice Resiliency Patterns. In Proc. IEEE International Conference on Software Architecture (ICSA'20). 2020. [Uses PRISM to model and analyse the behaviour of two popular microservice resiliency patterns: Retry and Circuit Breaker.]
  • [WLKV20] Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki and Moshe Y. Vardi. LTL_f Synthesis on Probabilistic Systems. In Proc. Int’l Symposium on Games, Automata, Logics, and Formal Verification (GandALF'20). 2020. [Presents techniques for finite-trace LTL and MDPs, with an implementation built on PRISM.]
  • [RWWDV20] Nima Roohi, Yu Wang, Matthew West, Geir E. Dullerud and Mahesh Viswanathan. STMC: Statistical Model Checker with Stratified and Antithetic Sampling. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 448-460, Springer. 2020. [bib] [Proposes a technique and tool for statistical model checking using antithetic and stratified sampling, built as an extension of PRISM.]
  • [Gle20] Mario Gleirscher. YAP: Tool Support for Deriving Safety Controllers from Hazard Analysis and Risk Assessments. In Proc. 2nd Workshop on Formal Methods for Autonomous Systems (FMAS'20). 2020. [Presents a tool for formal risk analysis including modelling and verification support from PRISM.]
  • [PTHH20] Kittiphon Phalakarn, Toru Takisaka, Thomas Haas and Ichiro Hasuo. Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), volume 12225 of LNCS, pages 349-371, Springer. 2020. [bib] [Develops a bounded value iteration technique for accurate solution of stochastic games, implemented as an extension of PRISM-games.]
  • [TH20] Iram Tariq Bhatti and Osman Hasan. Formal Verification of a Fully Automated Out-of-Plane Cell Injection System. In Proc. 21st International Symposium on Quality Electronic Design (ISQED'20), pages 111-116. 2020. [Uses probabilistic model checking and PRISM to analyse the functional correctness and performance of a fully automated out-of-plane cell injection system.]
  • [LCGS20] Nianyu Li, Javier Cámara, David Garlan and Bradley Schmerl. Reasoning about When to Provide Explanation for Human-involved Self-Adaptive Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20). 2020. [Reasons about self-adaptive systems with human involvement using probabilistic model checking and PRISM-games.]
  • [GGS20] T. J. Glazier, D. Garlan and B. Schmerl. Automated Management of Collections of Autonomic Systems. In Proc. IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS'20), pages 82-91. 2020. [Proposes an automated approach to managing multiple autonomic systems, building upon PRISM-games. ]
  • [KSHB20] Shamik Kundu, Ahmet Soyyiğit, Khaza Anuarul Hoque and Kanad Basu. High-level Modeling of Manufacturing Faults in Deep Neural Network Accelerators. In Proc. IEEE 26th International Symposium on On-Line Testing and Robust System Design (IOLTS'20). 2020. [Formally models and analyses faults in deep neural network accelerators using probabilistic model checking and PRISM.]
  • [MS20] MohammadSadegh Mohagheghi and Khayyam Salehi. Accelerating Interval Iteration for Expected Rewards in Markov Decision Processes. In Proc. 15th International Conference on Software Technologies (ICSOFT'20), pages 39-50. 2020. [Proposes efficient iterative methods for solving Markov decision processes, implemented as an extension of PRISM. ]
  • [LP20] Alessio Lomuscio and Edoardo Pirovano. Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. In Proc. 19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'20), pages 762-770. 2020. [Develops techniques and a tool for verifying parameterised probabilistic multi-agent systems, building upon PRISM and PRISM-games.]
  • [LP20b] Alessio Lomuscio and Edoardo Pirovano. Verifying Fault-Tolerance in Probabilistic Swarm Systems. In Proc. 29th International Joint Conference on Artificial Intelligence (IJCAI'20), pages 325-331. 2020. [Presents techniques for formally analysing fault-tolerance in unbounded robotic swarms, with an implementation that builds on PRISM.]
  • [XKSS20] Xin Xin, Sye Loong Keoh, Michele Sevegnani and Martin Saerbeck. Dynamic Probabilistic Model Checking for Sensor Validation in Industry 4.0 Applications. In Proc. IEEE International Conference on Smart Internet of Things (IEEE SmartIoT 2020), pages 43-50. 2020. [Proposes a run-time verification framework for sensor networks based on probabilistic model checking and PRISM.]
  • [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.]
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.]
  • [BBH+19] Nathalie Bertrand, Benjamin Bordais, Loïc Hélouët, Thomas Mari, Julie Parreaux and Ocan Sankur. Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking. In Proc. 3rd International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail'19), Springer. 2019. [Uses probabilistic model checking and PRISM to formally evaluate the performance of regulation algorithms in metro train lines.]
  • [KDL19] Gildas Kouko, Josée Desharnais and François Laviolette. Finite Approximation of LMPs for Exact Verification of Reachability Properties. In Proc. 16th International Conference on Quantitative Evaluation of Systems (QEST'19), volume 11785 of LNCS, pages 70-87, Springer. 2019. [Proposes techniques for approximate verification of labelled Markov processes using PRISM as an underlying solver.]
  • [EK19] Julia Eisentraut and Jan Kretinsky. Expected Cost Analysis of Attack-Defense Trees. In Proc. 16th International Conference on Quantitative Evaluation of Systems (QEST'19), volume 11785 of LNCS, pages 203-221, Springer. 2019. [bib] [Presents an approach to analysing attack-defence trees using PRISM-games for model checking stochastic games.]
  • [TAB+19] Martin Tappler, Bernhard K. Aichernig, Giovanni Bacci, Maria Eichlseder and Kim G. Larsen. L*-Based Learning of Markov Decision Processes. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 651-669, Springer. 2019. [Performs probabilistic model checking with PRISM as part of an MDP learning framework.]
  • [Mu19] Chunyan Mu. Automated Game-Theoretic Verification of Security Systems. In Proc. 16th International Conference on Quantitative Evaluation of SysTems (QEST'19), volume 11785 of LNCS, pages 239-256, Springer. 2019. [pdf] [bib] [Develops a game-theoretic approach to verifying security systems building upon PRISM.]
  • [NMMZZ19] Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng and Zhen Zhang. STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis. In Proc. 31st International Conference on Computer Aided Verification (CAV'19), volume 11561 of LNCS, pages 540-549, Springer. 2019. [Describes a tool for probabilistic verification of infinite-state systems, connecting to PRISM's model checking engines.]
  • [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.]
  • [ZRF+19] Xingyu Zhao, Valentin Robu, David Flynn, Fateme Dinmohammadi, Michael Fisher and Matt Webster. Probabilistic Model Checking of Robots Deployed in Extreme Environments. In Proc. Thirty-Third AAAI Conference on Artificial Intelligence. 2019. [Proposes a probabilistic model checking approach for verifying the safety of robots in hazardous environments, based on the use of PRISM.]
  • [SCRVP19] Gabriela Félix Solano, Ricardo Diniz Caldas, Genaína Nunes Rodrigues, Thomas Vogel and Patrizio Pelliccione. Taming Uncertainty in the Assurance Process of Self-Adaptive Systems: a Goal-Oriented Approach. In Proc. 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'19). 2019. [Proposes an assurance process for self-adaptive systems, with an implementation based on PRISM.]
  • [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.]
  • [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.]
2018
2017
2016
  • [IQV16] Paolo Izzo, Hongyang Qu and Sandor M. Veres. A stochastically verifiable autonomous control architecture with reasoning. In Proc. IEEE Conference on Decision and Control (CDC'16). 2016. [Proposes an architecture for autonomous control with underlying verification abilities provided by PRISM.]
  • [AC16] Jose Ignacio Aizpurua and Victoria M. Catterson. ADEPS: A Methodology for Designing Prognostic Applications. In Proc. 3rd European Conference of the Prognostics and Health Management Society. 2016. [Proposes ADEPS (Assisted Design for Engineering Prognostic Systems), which uses PRISM as an underlying verification tool.]
  • [KKR16] Lubos Korenciak, Antonin Kucera and Vojtech Rehak. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. In Proc. 24th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'16). 2016. [Proposes fixed-delay synthesis techniques on a variant of continuous-time Markov chains, implemented as an extension of PRISM.]
  • [KBC+16] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz and Steffen Märcker, David Müller. Advances in Symbolic Probabilistic Model Checking with PRISM. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), pages 349-366, Springer. 2016. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements. ]
  • [CDKB16] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat. In Proc. 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), volume 9633 of LNCS, pages 287-304, Springer. 2016. [Proposes a formalism for modelling families of probabilistic systems with differing features and a tool for their analysis, which connects to PRISM through model translations.]
  • [SAH+16] Muhammad Usama Sardar, Nida Afaq, Khaza Anuarul Hoque, Taylor T. Johnson and Osman Hasan. Probabilistic Formal Verification of the SATS Concept of Operation. In Proc. 8th International Symposium on NASA Formal Methods (NFM'16), volume 9690 of LNCS, pages 191–205, Springer. 2016. [Presents a formal analysis of NASA's Small Aircraft Transportation System (SATS) technology using probabilistic model checking and PRISM.]
  • [PLM16] Zhaoguang Peng, Yu Lu and Alice Miller. Uncertainty Analysis of Phased Mission Systems with Probabilistic Timed Automata. In Proc. 7th IEEE International Conference on Prognostics and Health Management (PHM'16). 2016. [Analyses phased mission requirements using probabilistic timed automata and PRISM.]
  • [GDH16] Paul Gainer, Clare Dixon and Ullrich Hustadt. Probabilistic Model Checking of Ant-Based Positionless Swarming. In Proc. Towards Autonomous Robotic Systems (TAROS'16). 2016. [Uses probabilistic model checking and PRISM to study control algorithms for robot swarms.]
  • [BKdM+16] Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier and Sascha Wunderlich. Greener Bits: Formal Analysis of Demand Response. In Proc. 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), pages 323-339, Springer. 2016. [Develops formal techniques for managing demand response in power generation, including a probabilistic analysis using PRISM. ]
  • [GEK16] Sotirios Gyftopoulos, Pavlos S. Efraimidis and Panagiotis Katsaros. Solving Influence Problems on the DeGroot Model with a Probabilistic Model Checking Tool. In Proc. 20th Pan-Hellenic Conference on Informatics (PCI'16). 2016. [Uses PRISM-games to analyse the DeGroot model of opinion diffusion and formation in social networks.]
  • [AH16] Mohammed Alabdullatif and Reiko Heckel. Graph Transformation Games for Negotiating Features. In Proc. Graphs as Models 2016. 2016. [Proposes a negotiation game for designing flexible business interactions, with an underlying analysis based on PRISM-games.]
  • [LZW+16] Lulu Liang, Kai Zheng, Zilong Wei, Yanmei Wang, Sihan Wu and Xin Huang. Model Checking of IoT System in Microgrid. In Proc. IEEE International Symposium on Information in Medicine and Education (ITME'16). 2016. [Verifies the reliability of IoT systems in microgrids using probabilistic model checking and PRISM.]
  • [CJP16] Radu Calinescu, Kenneth Johnson and Colin Paterson. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. In Proc. TACAS'16, volume 9636 of LNCS, pages 540-546, Springer. 2016. [Presents a model checker for computing confidence intervals, building on PRISM's parametric model checking functionality.]
  • [PMCG16] Ashutosh Pandey, Gabriel A. Moreno, Javier Cámara and David Garlan. Hybrid Planning for Decision Making in Self-Adaptive Systems. In Proc. 10th International Conference on Self-Adaptive and Self-Organizing Systems (SASO'16). 2016. [Presents a hybrid planning technique for self-adaptive systems combining learning and probabilistic model checking, with an implementation based on PRISM.]
  • [GBKF16] Safa Guellouz, Adel Benzina, Mohamed Khalgui, Georg Frey. ZiZo: A Complete Tool Chain for the Modeling and Verification of Reconfigurable Function Blocks. In Proc. 10th International Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies (UBICOMM'16). 2016. [Presents a tool-chain for modelling and verification of reconfigurable distributed system, using PRISM as a back-end verifier.]
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002

Theses

2021
2018
2015
2012
2011
2010
2009
2008
2007
2006
2004
2003

Technical reports

2011
2007
2005

Other

2005

Publications