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.

482 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

2021
  • [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.]
2020
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.]
  • [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.]
  • [SDK+20] Muhammad Usama Sardar, Clemens Dubslaff, Sascha Klüppelholz, Christel Baier and Akash Kumar. Performance Evaluation of Thermal-Constrained Scheduling Strategies in Multi-core Systems. In Proc. European Workshop on Performance Engineering (EPEW'19), volume 12039 of LNCS, pages 133-147, Springer. 2019. [Performs formal verification of scheduling strategies for multi-core systems using PRISM.]
  • [DCV+19] Nicolas Dejon, Davide Caputo, Luca Verderame, Alessandro Armando and Alessio Merlo. Automated Security Analysis of IoT Software Updates. In Proc. IFIP International Conference on Information Security Theory and Practice (WISTP'19), Springer. 2019. [Presents the automated software analysis framework IoTAV, which uses PRISM as an underlying model checker.]
  • [MWA19] Gareth W. Molyneu, Viraj B. Wijesuriya and Alessandro Abate. Bayesian Verification of Chemical Reaction Networks. In Proc. International Symposium on Formal Methods (FM'19) Workshops, pages 461-479. 2019. [Presents a bayesian approach to verification of chemical reaction networks, using PRISM's parametric model checking functionality.]
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. [bib] [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