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.

 

Sort by: date, type, title, subject

340 publications:

Book chapters

2009

Journal papers

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

Conference papers

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.]
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.]
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.]
  • [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.]
  • [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.]
  • [CGSP15] Javier Cá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. [Proposes techniques for architecture-based self-adapation using stochastic multi-player games and PRISM-games.]
  • [BCFK15] Tomáš Brázdil, Krishnendu Chatterjee, Vojtěch Forejt and Antonín Kučera. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of LNCS, pages 181-187, Springer. 2015. [Presents a tool for multi-objective model checking of mean-payoff properties MDPs, building on several PRISM components.]
  • [RGH15] Daniël Reijsbergen, Stephen Gilmore and Jane Hillston. Patch-based Modelling of City-centre Bus Movement with Phase-type Distributions. In Proc. 7th International Workshop on Practical Applications of Stochastic Modelling (PASM'14), volume 310 of ENTCS, pages 157-177. 2015. [Uses HyperStar and PRISM on a stochastic performance model of a public transportation network.]
  • [CMG15] Javier Cámara, Gabriel A. Moreno and David Garlan. Reasoning about Human Participation in Self-Adaptive Systems. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes a formal framework for reasoning about human involvement in self-adaptive systems, using PRISM-games as an underlying model checker.]
  • [CGLG15] Zack Coker, David Garlan and Claire Le Goues. SASS: Self-adaptation using stochastic search. In Proc. 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'15). 2015. [Proposes the use of stochastic search techniques for self-adaptive systems, illustrated with a genetic algorithm that uses PRISM to compute fitness functions.]
  • [CGB15] Radu Calinescu, Simos Gerasimou and Alec Banks. Self-Adaptive Software with Decentralised Control Loops. In Proc. 18th International Conference on Fundamental Approaches to Software Engineering (FASE'15). 2015. [Presents an approach for decentralised control of self-adaptive systems, using PRISM as an underlying model checker.]
  • [NSG+15] Athanasios Naskos, Emmanouela Stachtiari, Anastasios Gounaris, Panagiotis Katsaros, Dimitrios Tsoumakos, Ioannis Konstantinou and Spyros Sioutas. Dependable Horizontal Scaling Based On Probabilistic Model Checking. In Proc. 15th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGrid'15). 2015. [Uses probabilistic model checking and PRISM for cloud elasticity, i.e. on-demand resource provisioning in cloud computing.]
  • [PLK+15] Jaime Pulido Fentanes, Bruno Lacerda, Tomas Krajnik, Nick Hawes and Marc Hanheide. Now or later? Predicting and Maximising Success of Navigation Actions from Long-Term Experience. In Proc. 2015 IEEE International Conference on Robotics and Automation (ICRA'14). 2015. [Proposes novel approaches to predicting changes in a robot's environment, applied to a probabilistic planning framework using PRISM as an underlying solver.]
  • [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.]
  • [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 Cá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 Cá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.]
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002

Theses

2015
2012
2011
2010
2009
2008
2007
2006
2004
2003

Technical reports

2011
2007
2005

Other

2005

Sort by: date, type, title, subject

Publications