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.

629 publications:

Tool/language connections to PRISM (237)

2024
2023
2022
2021
2020
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
2017
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
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002

Extensions and adaptions to PRISM (62)

2024
2023
  • [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
2021
2020
2019
2018
2017
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
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
2010
2009
2008
2007
2005

Case studies using PRISM (329)

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

Publications