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

526 publications:

Book chapters

2009

Journal papers

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

Conference papers

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

Sort by: date, type, title, subject

Publications