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

378 publications:

Book chapters

2009

[CGHV09] M. Calder, S. Gilmore, J. Hillston and V. Vyshemirsky. Formal methods for biochemical signalling pathways. In Formal Methods: State of the Art and New Directions, Springer. To appear. 2009. [bib]

Journal papers

2019

[UAU+19] Riaz Uddin, Ali S. Alghamdi, Muhammad Hammad Uddin, Ahmed Bilal Awan and Syed Atif Naseem. Ethernet-Based Fault Diagnosis and Control in Smart Grid: A Stochastic Analysis via Markovian Model Checking. Journal of Electrical Engineering & Technology. 2019. [Formally analyses the reliability of fault detection, isolation and supply restoration (FDIR), including use of PRISM.]
[NKI19] Ali A. Noroozi, Jaber Karimpour and Ayaz Isazadeh. Information leakage of multi-threaded programs. Computers & Electrical Engineering, 78, pages 400-419. 2019. [Presents an approach for quantitative information flow, implemented in PRISM-Leak, an extension of PRISM.]
[SKII19] Khayyam Salehi, Jaber Karimpour, Habib Izadkhah and Ayaz Isazadeh. Channel Capacity of Concurrent Probabilistic Programs. Entropy, 21(9). 2019. [Studies information leakage for concurrent probabilistic programs using an extension of PRISM.]
[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.]

2018

[MCDMR18] Giovanni Mazzeo, Luigi Coppolino, Salvatore D’Antonio, Claudio Mazzariello and Luigi Romano. SIL2 Assessment of an Active/Standby COTS-Based Safety-related System. Reliability Engineering & System Safety. 2018. [Proposes an approach to safety certification for Commercial-Off-The-Shelf (COTS) components using PRISM.]
[KML+18] Justus A. Kromer, Steffen Märcker, Steffen Lange, Christel Baier and Benjamin M. Friedrich. Decision making improves sperm chemotaxis in the presence of noise. Computational Biology, 14(4). 2018. [Uses probabilistic model checking and PRISM to study decision making in sperm chemotaxis.]
[CDKB+18] Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. ProFeat: Feature-oriented Engineering for Family-based Probabilistic Model Checking. Formal Aspects of Computing, volume, 30(1), pages 45-75. 2018. [Presents the ProFeat tool for feature-oriented modelling and feature-aware analysis, incorporating PRISM.]
[KBC+18] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer, 20(2), pages 179-194. 2018. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements.]
[LJ18] Nian-Ze Lee and Jie-Hong R. Jiang. Towards Formal Evaluation and Verification of Probabilistic Design. IEEE Transactions on Computers, 67(8), pages 1202-1216, IEEE. 2018. [Uses PRISM as part of a framework to verify approximate and probabilistic designs for circuits.]
[TMR18] Pedro J. Rivera Torres, E. I. Serrano Mercado and E. I. Serrano Mercado. Probabilistic Boolean Network Modeling of an Industrial Machine. Journal of Intelligent Manufacturing. 2018. [Uses Probabilistic Boolean Networks to model manufacturing processes, and analyses models using PRISM.]

2017

[KBC+17] Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer. 2017. [Presents a collection of extensions to PRISM, including automatic variable reordering, reward-based properties and automata improvements.]
[MSHA17] Mujahid Mohsin, Muhammad Usama Sardar, Osman Hasan and Zahid Anwar. IoTRiskAnalyzer: A Probabilistic Model Checking Based Framework for Formal Risk Analytics of the Internet of Things. IEEE Access, IEEE. 2017. [Presents a framework for formally quantifying risk in Internet of Things applications, using PRISM as the underlying probabilistic model checker.]

2016

[TMSR16] Pedro J. Rivera Torres, Eileen I. Serrano Mercado, Orestes Llanes Santiago and Luis Anido Rifon. Modeling preventive maintenance of manufacturing processes with probabilistic Boolean networks with interventions. Journal of Intelligent Manufacturing, Springer. 2016. [Proposes techniques based on probabilistic Boolean networks to analyse manufacturing processes, and uses PRISM as an underlying tool.]
[NGMK16] Athanasios Naskos, Anastasios Gounaris, Haralambos Mouratidis and Panagiotis Katsaros. Online analysis of security risks in elastic cloud applications using probabilistic model checking. IEEE Cloud Computing Magazine. 2016. [Analyses the trade-offs between security risks and performance in cloud computing systems using probabilistic model checking and PRISM.]
[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

[KG15] Savas Konur and Marian Gheorghe. A Property-Driven Methodology for Formal Analysis of Synthetic Biology Systems. IEEE/ACM Transactions on Computational Biology and Informatics. 2015. [Proposes a framework for formal analysis of synthetic biology systems, which includes use of PRISM for probabilistic model checking.]
[CCDR15] Giuseppe Cicotti, Luigi Coppolino, Salvatore D'Antonio and Luigi Romano. Runtime Model Checking for SLA Compliance Monitoring and QoS Prediction. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, 6(2). 2015. [Proposes a QoS prediction approach using PRISM and applied to a smart grid case study.]
[TMR15] Pedro J. Rivera-Torres, E.I. Serrano Mercado and Anido L. Rifon. Probabilistic Boolean network modeling and model checking as an approach for DFMEA for manufacturing systems. Journal of Intelligent Manufacturing, pages 1-21, Springer. 2015. [Uses probabilistic Boolean networks and PRISM to analyse automated manufacturing assembly processes.]
[TTL14] Anton Tarasyuk, Elena Troubitsyna and Linas Laibinis. Integrating stochastic reasoning into Event-B development. Formal Aspects of Computing, 27, pages 53–77. 2015. [Describes an extension of Event-B for stochastic reasoning, using PRISM to perform probability calculations.]
[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.]
[CGJ+15] Radu Calinescu, Carlo Ghezzi, Kenneth Johnson, Mauro Pezzé, Yasmin Rafiq and Giordano Tamburrelli. Formal Verification With Confidence Intervals to Establish Quality of Service Properties of Software Systems. IEEE Transactions on Reliability. 2015. [Uses PRISM as part of a tool chain formally verify QoS properties of software systems.]
[LMO15] Gabriele Lenzini, Sjouke Mauw and Samir Ouchani. Security Analysis of Socio-Technical Physical Systems. Computers & Electrical Engineering, Elsevier. 2015. [Proposes an approach to detect and quantify attacks in socio-technical physical systems, using a mapping to PRISM.]
[JKG15] Benjamin Johnson and Hadas Kress-Gazit. Analyzing and revising synthesized controllers for robots with sensing and actuation errors. International Journal of Robotics Research, 34(6), pages 816-832. 2015. [Uses probabilistic model checking and PRISM for the synthesis of verifiable robot controllers.]

2014

[GCB+14] Felipe Pontes Guimaraes, Pedro Célestin, Daniel Macedo Batista, Genaína Nunes Rodrigues and Alba Cristina Magalhaes Alves de Melo. A Framework for Adaptive Fault-Tolerant Execution of Workflows in the Grid: Empirical and Theoretical Analysis. Journal of Grid Computing, 12(1), pages 127-151, Springer. 2014. [Proposes a framework for adaptive fault-tolerant execution of workflows in the grid, including dependability analysis with PRISM. ]
[KH14] Koichi Kobayashi and Kunihiko Hiraishi. Verification and Optimal Control of Context-Sensitive Probabilistic Boolean Networks Using Model Checking and Polynomial Optimization. The Scientific World Journal. 2014. [Presents various techniques for analysing probabilistic Boolean networks, including one that uses probabilistic model checking and PRISM.]
[SBN14] Pravati Swain, Purandar Bhaduri and Sukumar Nandi. Probabilistic model checking of IEEE 802.11 IBSS power save mode. International Journal of Wireless and Mobile Computing, 7(7), pages 465-474. 2014. [Uses probabilistic model checking and PRISM to analyse a power management algorithm for Independent Basic Service Set (IBSS) from the IEEE 802.11 standard for wireless local area networks.]
[SBWA14] Khalid Sultan, Jamal Bentahar, Wei Wan and Faisal Al-Saqqar. Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments. Expert Systems with Applications, 41(14), pages 6291-6304, Elsevier. 2014. [Proposes techniques for analysing probabilistic multi-agent systems, implemented using PRISM.]
[CS14] Muffy Calder and Michele Sevegnani. Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Aspects of Computing, 26(3), pages 537-561. 2014. [Analyses a model of the 802.11 CSMA/CA RTS/CTS protocol, modelled in an extension of stochastic bigraphical reactive systems, and then imported into PRISM]
[HMST14] Khaza Anuarul Hoque, Otmane Ait Mohamed, Yvon Savaria and Claude Thibeault . Early Analysis of Soft Error Effects for Aerospace Applications Using Probabilistic Model Checking. Formal Techniques for Safety-Critical Systems Communications in Computer and Information Science, 419, pages 54-70, Springer. 2014. [Uses probabilistic model checking and PRISM to analyse dependability and performability properties of SRAM-based FPGAs.]
[JD14] Yosr Jarraya and Mourad Debbabi. Quantitative and qualitative analysis of SysML activity diagrams. International Journal on Software Tools for Technology Transfer, 16(4), pages 399-419. 2014. [Presents a framework for probabilistic verification of SysML activity diagrams via a translation to PRISM.]
[SBE14] Khalid Sultan, Jamal Bentahar and Mohamed El-Menshawy. Model checking probabilistic social commitments for intelligent agent communication. Applied Soft Computing, 22, pages 397-409, Elsevier. 2014. [Performs probabilistic model checking of commitments in multi-agent systems via connection to PRISM.]
[RC14] José Ignacio Requeno and José Manuel Colom. Analyzing phylogenetic trees with timed and probabilistic model checking: the lactose persistence case study. Journal of Integrative Bioinformatics, 11(3). 2014. [Analyses phylogenetic trees using probabilistic model checking and PRISM.]
[PLM+14] Zhaoguang Peng, Yu Lu, Alice Miller, Tingdi Zhao and Chris Johnson. Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites. Quality and Reliability Engineering International. 2014. [Uses probabilistic model checking and PRISM to analyse reliability, availability and maintainability properties of a satellite system.]
[OMD14] Samir Ouchani, Otmane Aït Mohameda and Mourad Debbabi. A property-based abstraction framework for SysML activity diagrams. Knowledge-Based Systems, 6, pages 328-343. January 2014. [Presents methods to abstract and verify SysML activity diagrams using PRISM as a back-end.]

2013

[SGO13] Simon Struck, Matthias Gudemann and Frank Ortmeier. Efficient Optimization of Large Probabilistic Models. Journal of Systems and Software. 2013. [Presents a framework for modelling, analysis and optimization of safety critical systems, which connects to PRISM.]
[Tsa13] Tony Tsang. Performance Analysis for QoS-Aware Two- Layer Scheduling in LTE Networks. International Journal of Emerging Trends & Technology in Computer Science (IJETTCS), 2(2). 2013. [Uses an extension of PRISM's simulator to solve scheduling and resource allocation problems.]
[KV13] Jayanand Asok Kumar and Shobha Vasudevan. Formal Probabilistic Timing Verification in RTL. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(5), pages 788-801, IEEE. 2013. [Analyses timing properties of RTL designs, using the SHARPE tool and a connection to PRISM.]
[PTA13] Anna Philippou, Mauricio Toro and Margarita Antonaki. Simulation and Verification for a Process Calculus for Spatially-explicit Ecological Models. Scientific Annals of Computer Science, 23(1), pages 119–167. 2013. [Develops a stochastic process algebra for locations/populations called PALPS, with a translation into PRISM for probabilistic model checking.]
[GMZ13] H. Gao, H. Miao and H. Zeng. Predictive web service monitoring using probabilistic model checking. International Journal on Applied Mathematics & Information Sciences, 6(1L), pages 139–148. 2013. [Uses probabilistic model checking and PRISM to predict web service reliability.]
[RSLG13] Mikołaj Rybiński, Zuzanna Szymańska, Sławomir Lasota and Anna Gambin. Modelling the efficacy of hyperthermia treatment. J. R. Soc. Interface, 10(88). 2013. [Analyses models of the effectiveness of hyperthermia in the context of a heat-shock response mechanism, using ODEs and PRISM.]
[KFDK13] Savas Konur, Michael Fisher, Simon Dobson and Stephen Knox. Formal Verification of a Pervasive Messaging System. Formal Aspects of Computing. 2013. [Uses PRISM to apply probabilistic model checking to the analysis of a pervasive message-forwarding system called Scatterboxs]
[Kik13] Shinji Kikuchi. Using Model Checking to Evaluate Live Migrations. IT Professional, 15(2), pages 36-41, IEEE Computer Society. 2013. [Uses probabilistic model checking and PRISM to analyse live migration strategies for cloud computing.]
[HS13] Luke Herbert and Robin Sharp. Precise Quantitative Analysis of Probabilistic Business Process Model and Notation Workflows. J. Comput. Inf. Sci. Eng., 13(1). 2013. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows.]
[CK13] Lalit Chandnani and Hemangee K. Kapoor. Formal Approach for DVS-Based Power Management for Multiple Server System in Presence of Server Failure and Repair. IEEE Transactions On Industrial Informatics, 9(1), pages 502-513. 2013. [Uses PRISM to analyse a novel DVS-based power management policy for multiprocessor systems.]
[PBR13] Sophia Petridou, Stylianos Basagiannis and Manos Roumeliotis. Survivability Analysis Using Probabilistic Model Checking: A Study on Wireless Sensor Networks. IEEE Systems Journal, 7(1), pages 4-12. 2013. [Analyses survivability properties of wireless sensor networks using PRISM.]
[YPH13] Guofeng Yan, Yuxing Peng and Bin Huang. State Reachability of Wireless Lossy Channel Systems: Modeling and Probabilistic Analyzing. Journal of Computational Information Systems, 9(4), pages 1381–1388. 2013. [Analyses wireless lossy channel systems using PRISM.]
[Kap13] Tatjana Kapus. Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata. Mobile Information Systems, 9(2), pages 157-188, IOS Press. 2013. [Uses PRISM to build and analyse a probabilistic timed automaton model of the medium access control in nonbeacon-enabled IEEE 802.15.4 wireless personal area networks.]
[CDF+13] Andrea Ciancone, Mauro Luigi Drago, Antonio Filieri, Vincenzo Grassi, Heiko Koziolek and Raffaela Mirandola. The KlaperSuite Framework for Model-Driven Reliability Analysis of Component-Based Systems. Software & Systems Modeling. 2013. [Describes the KlaperSuite framework for model-driven reliability analysis, which builds on several tools including PRISM.]

2012

[BMJM12] S. Bhatti, S. Memon, I.A. Jokhio and M.A. Memon. Modelling and symmetry reduction of a target-tracking protocol using wireless sensor networks. IET Communications, 6(10), pages 1205-1211. 2012.
[LPA+12] Pietro Liò, Nicola Paoletti, Mohammad Ali Moni, Kathryn Atwell, Emanuela Merelli and Marco Viceconti. Modelling osteomyelitis. BMC Bioinformatics, 13(Suppl 14)(S12). 2012. [Describes computational modelling of the bone pathology osteomyelitis, part of which is analysed using PRISM.]
[RASL12] Genaína Nunes Rodrigues, Vander Alves, Renato Silveira and Luiz A. Laranjeira. Dependability Analysis in the Ambient Assisted Living Domain: An Exploratory Case Study. Journal of Systems and Software, 85(1), pages 112-131. 2012. [bib] [Uses PRISM to analyse dependability properties of Ambient Assisted Living systems.]
[KDF12] Savas Konur, Clare Dixon and Michael Fisher. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems, 60(2), pages 199-213. 2012. [bib] [Uses probabilistic model checking and PRISM to analyse the effectiveness of robot swarms.]
[RLB+12] Mikolaj Rybinski, Michal Lula, Pawel Banasik, Slawomir Lasota and Anna Gambin. Tav4SB: Integrating tools for analysis of kinetic models of biological systems. BMC Systems Biology, 6(25). 2012.
[KSBH12] Heiko Koziolek, Bastian Schlich, Steffen Becker and Michael Hauck. Performance and reliability prediction for evolving service-oriented software systems. Empirical Software Engineering. To appear. 2012.
[GMS+12] Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe Ferri and Edson Watanabe. Constructive model-based analysis for safety assessment. International Journal on Software Tools for Technology Transfer (STTT). 2012. [Uses PRISM in a quantitative safety assessment framework via model translation from Simulink.]
[OJMD12] Samir Ouchani, Yosr Jarraya, Otmane Ait Mohamed and Mourad Debbabi. Probabilistic Attack Scenarios to Evaluate Policies over Communication Protocols. Journal of Software, 7(7), pages 1488-1495. 2012. [Analyses communication protocol attack scenarios with PRISM, using RTSP/SRTP as an example.]
[AC12] Oana Andrei and Muffy Calder. Trend-Based Analysis of a Population Model of the AKAP Scaffold Protein. Transactions on Computational Systems Biology, XIV, pages 1-25, Springer. 2012. [Studies the AKAP scaffold protein by introducing a notion of stochastic trends and using PRISM for model analysis.]
[YTP+12] Qixia Yuan, Panuwat Trairatphisan, Jun Pang, Sjouke Mauw, Monique Wiesinger and Thomas Sauter. Probabilistic Model Checking of the PDGF Signaling Pathway. Transactions on Computational Systems Biology, XIV, pages 151-180. 2012. [Analyses the PDGF signalling pathway using PRISM.]
[CCN12] Luca Cardelli and Attila Csikász-Nagy. The Cell Cycle Switch Computes Approximate Majority. Nature Scientific Reports, 2. 2012. [Studies the cell cycle switch as a computing device, based on deterministic/stochastic simulation and probabilistic verification with PRISM.]
[MMAG12] Indika Meedeniya, Irene Moser, Aldeida Aleti and Lars Grunske. Evaluating Probabilistic Models with Uncertain Model Parameters. Software and Systems Modelling, Springer. 2012. [Proposes techniques to evaluate probabilistic models with uncertainty, using PRISM as a back-end solution engine.]
[KH12] K. Kobayashi and K. Hiraishi. Symbolic approach to verification and control of deterministic/probabilistic Boolean networks. IET Systems Biology, 6(6), pages 215-222. 2012. [Applies PRISM to the analysis of probabilistic Boolean networks, using an apoptosis network and a WNT5A network as examples.]

2011

[DDBM11] M. P. Dobay, A. Dobay, J. Bantang and E. Mendoza. How many trimers? Modeling influenza virus fusion yields a minimum aggregate size of six trimers, three of which are fusogenic. Molecular BioSystems. 2011. [bib]
[JGB11] Paul Jennings, Arka Ghosh and Samik Basu. A Two-phase Approximation for Model Checking Unbounded Until Properties of Probabilistic Systems. ACM Transactions on Software Engineering and Methodology. 2011. [bib]
[STTT11] Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi and Kazuko Takahashi. Probabilistic Symmetry Reduction for a System with Ring Buffer. IEICE Transactions, 94-D(5), pages 967-975. 2011. [bib]
[MZ11] Ravie C. Muniyandi and Abdullah M. Zin. Membrane Computing as a Modeling Tool for Discrete Systems. Journal of Computer Science, 7(11), pages 1667-1673. 2011. [bib]
[MZ11b] Ravie C. Muniyandi and Abdullah M. Zin. Evaluating Ligand-Receptor Networks of TGF-β with Membrane Computing. Pakistan Journal of Biological Sciences, 14, pages 1100-1108. 2011. [bib]
[NIOK11] T. Nagaoka and A. Ito and K. Okano and S. Kusumoto. QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation. IEICE Transactions on Information and Systems, E94.D(5), pages 958-966 . 2011.
[BPA+11] Stylianos Basagiannis, Sophia Petridou, Nikolaos Alexiou, Georgios Papadimitriou and Panagiotis Katsaros. Quantitative analysis of a certified e-mail protocol in mobile environments: A probabilistic model checking approach. Computers & Security, 30(4), pages 257–272, Elsevier. 2011. [bib] [Analyses the Certified E-mail Message Delivery (CEMD) protocol using PRISM.]
[CFCC11] Mirlaine A Crepalde, Alessandra C Faria-Campos and Sérgio VA Campos. Modeling and analysis of cell membrane systems with probabilistic model checking. BMC Genomics, 12(Suppl 4)(S14). 2011. [Analyses a sodium-potassium exchange pump using probabilistic model checking and PRISM.]

2010

[AL10] H. Aljazzar and S. Leue. Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking. IEEE Transactions on Software Engineering, 36(1), pages 37-60, IEEE Computer Society. 2010. [bib]
[RMH10] C. Rohr, W. Marwan and M. Heiner. Snoopy - A unifying Petri net framework to investigate biomolecular networks. Bioinformatics, 26(7), pages 974-975. 2010. [bib]
[ZYXL10] Yefei Zhao, Zongyuan Yang, Jinkui Xie and Qiang Liu. Quantitative Analysis of System Based on Extended UML State Diagrams and Probabilistic Model Checking. Journal of Software, 5(7), pages 793-800. 2010. [bib]
[ZBB10] Hafedh Zayani, Kamel Barkaoui and Rahma Ben Ayed. Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol. International Journal of Wireless & Mobile Networks, 2(2), pages 156-170. 2010. [bib]

2009

[BKPA09] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. Probabilistic model checking for the quantification of DoS security threats. Computers & Security, Elsevier. 2009. [bib]
[HHWZ09] H. Hermanns, E. M. Hahn, B. Wachter and L. Zhang. Time-bounded model checking of infinite-state continuous-time Markov chains. Fundamenta Informaticae, 95(1), pages 129-155. 2009. [bib]
[STTK09] Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Koichi Takahashi and Tohru Kikuno. Probabilistic Model Checking of the One-Dimensional Ising Model. IEICE Transactions on Information and Systems, E92.D(5), pages 1003-1011. 2009. [bib]
[BG+09] M. ter Beek, S. Gnesi, D. Latella, M. Massink, M. Sebastianis and G. Trentanni. Assisting the Design of a Groupware System - Model Checking Usability Aspects of thinkteam. Journal of Logic and Algebraic Programming, 78(4), pages 191-232, Elsevier. April 2009. [bib]

2008

[ERE08] A. El Rayes and M. Er. Using the Probabilistic Model Checker PRISM to Analyze Credit Card Use. Electronic Journal of Information Systems Evaluation, 11(1). 2008. [bib]
[SDM08] A. Sesic, S. Dautovic and V. Malbasa. Dynamic Power Management of a System With a Two-Priority Request Queue Using Probabilistic-Model Checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(2). February 2008. [bib] http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=4435957&arnumber=4378215

2007

[MM07] A. McIver and C. Morgan. Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic, 8(1). 2007. [bib]
[SMA+07] A. Susu, M. Magno, A. Acquaviva, D, Atienzay and G. De Micheli. Reconfiguration Strategies for Environmentally Powered Devices: Theoretical Analysis and Experimental Validation. Transactions on High-Performance Embedded Architectures and Compilers, 1(1), pages 327-346. January 2007. [bib] http://si2.epfl.ch/~susu/pubs.html
[RBB07] G. Roelke, R. Baldwin and D. Bulutoglu. Analytical Models for the Performance of von Neumann Multiplexing. IEEE Transactions on Nanotechnology, 6(1), pages 75-89. January 2007. [bib] http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4063343

2006

[CVGO06] M. Calder, V. Vyshemirsky, D. Gilbert and R. Orton. Analysis of signalling pathways using continuous time Markov chains. Transactions on Computational Systems Biology VI, 4220, pages 44-67, Springer. 2006. [bib] http://www.dcs.gla.ac.uk/~muffy/papers.html
[FP06] W. Fokkink and J. Pang. Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM. Journal of Universal Computer Science, 12(8), pages 981--1006. 2006. [bib] http://www.jucs.org/jucs_12_8/variations_on_itai_rodeh
[CB06] D. Chu and I. Blomfield. Orientational control is an efficient control mechanism for phase switching in the E.coli fim system. Journal of Theoretical Biology, Elsevier. To appear. 2006. [bib] http://www.cs.kent.ac.uk/people/staff/dfc/site/
[BSGG06] D. Bhaduri, S. Shukla, P. Graham and M. Gokhale. Comparing Reliability-Redundancy Trade-offs for Two Von Neumann Multiplexing Architectures. IEEE Transactions on Nanotechnology. To appear. 2006. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html
[Ste06] G. Steel. Formal Analysis of PIN Block Attacks. Theoretical Computer Science, 367(1-2), pages 257-270, Elsevier. 2006. [bib]

2005

[GK05] S. Gilmore and L. Kloul. A Unified Tool for Performance Modelling and Prediction. Reliability Engineering and System Safety, 89(1), pages 17-32, Elsevier. To appear. July 2005. http://www.sciencedirect.com/
[BCM+05] R. Barbuti, S. Cataudella, A. Maggiolo-Schettini, P. Milazzo and A. Troina. A Probabilistic Model for Molecular Systems. Fundamenta Informaticae, 67(1-3), pages 13-27. July 2005. [bib] http://www.di.unipi.it/~milazzo/
[MM05a] A. McIver and C. Morgan. An elementary proof that Herman's Ring is THETA(N-squared). Information Processing Letters, 94(2), pages 79-84. April 2005. [bib] http://www.cse.unsw.edu.au/~carrollm/probs/Papers/McIver-05c.pdf
[ISSG05] S. Irani, G. Singh, S. Shukla and R. Gupta. An Overview of the Competitive and Adversarial Approaches to Designing Dynamic Power Management Strategies. IEEE Transactions on VLSI Systems. 2005. [bib] http://www.cse.ucsd.edu/~gupta/pubs/TVLSIEnergy05.pdf

2004

[Shm04] V. Shmatikov. Probabilistic Model Checking of an Anonymity System. Journal of Computer Security, 12(3/4), pages 355-377. 2004. [bib] http://www.cs.utexas.edu/~shmat/index.html

2003

[GHB+03] M. Gribaudo, A. Horvath, A. Bobbio, E. Tronci, E. Ciancamerla and M. Minichino. Fluid Petri Nets and Hybrid Model-checking: A Comparative Case Study. Reliability Engineering and System Safety, 81, pages 239-257. 2003. [bib] http://www.mfn.unipmn.it/~bobbio/BIBLIO/bliagg.html

Conference papers

2020

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

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

2018

[LP18] Alessio Lomuscio and Edoardo Pirovano. Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems. In Proc. 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI'18), AAAI Press. 2018. https://www.ijcai.org/proceedings/2018/0056.pdf [Proposes verification techniques for probabilistic swarm systems, including an implementation that uses PRISM.]
[NF18] Mehran Alidoost Nia and Fathiyeh Faghih. Probabilistic Analysis of Self-Stabilizing Systems: A Case Study on a Mutual Exclusion Algorithm. In Proc. 2018 Real-Time and Embedded Systems and Technologies (RTEST'18), IEEE. 2018. [Uses PRISM to analyse and improve a mutual exclusion algorithm.]
[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.]
[WBD+08] Matt Webster, Michael Breza, Clare Dixon, Michael Fisher and Julie McCann. Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks. In Proc. Automated Verification of Critical Systems 2018 (AVoCS'18) . 2018. [Verifies protocols for wireless sensor networks using probabilistic model checking and PRISM.]

2017

[ZBDL17] Xi Zheng, Matthew L. Bolton, Christopher Daly and Lu Feng. A Formal Human Reliability Analysis of a Community Pharmacy Dispensing Procedure. In Proc. Human Factors and Ergonomics Society 2017 Annual Meeting, pages 728-732. 2017. [Uses probabilistic model checking and PRISM to predict medication error rates and explore interventions in pharmacy dispensing procedures.]
[SH17] Muhammad Usama Sardar and Osman Hasan. Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems. In Proc. Models for Formal Analysis of Real Systems (MARS'17), pages 271-282. 2017. [Models and analyses robotic cell injection systems using PRISM.]
[WJW+17] Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen and Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. In Proc. 56th Annual Conference on Decision and Control (CDC'17), pages 2201-2208, IEEE. 2017. [Develops a game-based abstraction approach to solving POMDPs, including PRISM-games as part of the tool-chain.]
[SBJJB17] Jiyoung Song, Young-Min Baek, Mingyu Jin, Eunkyoung Jee and Doo-Hwan Bae. SoS GaP Slicer: Slicing SoS Goal and PRISM Models for Change-Responsive Verification of SoS. In Proc. 2017 24th Asia-Pacific Software Engineering Conference (APSEC'17). 2017. [Presents a slicing technique, based on PRISM models, for statistical model checking of system-of-system models.]
[SCA+17] Gautham Nayak Seetanadi, Javier Cámara, Luis Almeida, Karl-Erik Årzén and Martina Maggio. Event-Driven Bandwidth Allocation with Formal Guarantees for Camera Networks. In Proc. 2017 IEEE Real-Time Systems Symposium (RTSS'17), pages 243-254. 2017. [Uses PRISM to verify a bandwidth allocation scheme for camera networks.]
[BKKW17] Christel Baier, Joachim Klein, Sascha Kluppelholz and Sascha Wunderlich. Maximizing the Conditional Expected Reward for Reaching the Goal. In In Proc. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Springer. 2017. [Introduces novel techniques for computing conditional expected rewards in MDPs, implemented in an extension of PRISM.]
[AVA+17] Arthur Americo, Artur Vaz, Mario S. Alvim, Sergio V. A. Campos and Annabelle McIver. Formal Analysis of the Information Leakage of the DC-Nets and Crowds Anonymity Protocols. In Proc. Brazilian Symposium on Formal Methods, pages 142-158, Springer. 2017. [Studies information leakage in anonymity protocols, building on probabilistic model checking with PRISM.]

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.]
[CC15] Giuseppe Cicotti and Antonio Coronato. Towards a Probabilistic Model Checking-based approach for Medical Device Risk Assessment. In Proc. IEEE International Workshop on Medical Measurement and Applications (MEMEA'15). 2015. [Uses probabilistic model checking and PRISM in a new approach for quantitative medical device risk assessment.]
[ZWC+15] Conghua Zhou, Yong Wang, Meiling Cao, Jianqi Shi and Yang Liu. Formal Analysis of MAC in IEEE 802.11p with Probabilistic Model Checking. In Proc. International Symposium on Theoretical Aspects of Software Engineering (TASE'15), pages 55-62, IEEE. 2015. [Uses probabilistic model checking and PRISM to analyse 802.11p for vehicular ad-hoc networks.]
[RMT15] Arunkumar Ramaswamy, Bruno Monsuez and Adriana Tapus. Model-driven self-adaptation of robotics software using probabilistic approach. In Proc. 2015 European Conference on Mobile Robots (ECMR'15). 2015. [Uses PRISM as part of a framework for model-driven self-adaptation of robotics software.]
[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 Cá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 Cá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 Cá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 Cá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

[HBHS14] Fenglin Han, Jan Olaf Blech, Peter Herrmann and Heinz Schmidt. Towards Verifying Safety Properties of Real-Time Probabilistic Systems. In Proc. Formal Engineering Approaches to Software Components and Architectures (FESCA'14), EPTCS. 2014. [Presents an extension of the Reactive Blocks tool set for analysing probabilistic real-time systems, through a connection to PRISM.]
[HHJC14] Luke Herbert, Zaza Nadja Lee Hansen, Peter Jacobsen and Pedro Cunha. Evolutionary optimization of production materials workflow processes. In Proc. 8th International Conference on Digital Enterprise Technology (DET'14). 2014. [Presents evolutionary optimisation techniques for stochastic production processes, using PRISM as an underlying model checker.]
[GPST14] Carlo Ghezzi, Mauro Pezzè, Michele Sama and Giordano Tamburrelli. Mining Behavior Models from User-Intensive Web Applications. In Proc. ICSE'14. 2014. [Proposes techniques to infer probabilistic behaviour models from web application logs and analyses the models using PRISM.]
[SCG+14] Bradley Schmerl, Javier Cámara, Jeffrey Gennari, David Garlan, Paulo Casanova, Gabriel A. Moreno, Thomas J. Glazier and Jeffrey M. Barnes. Architecture-based self-protection: composing and reasoning about denial-of-service mitigations. In Proc. 2014 Symposium and Bootcamp on the Science of Security (HotSoS'14). 2014. [Proposes adaptive techniques for denial-of-service mitigation, including formal analysis of adaptation strategies using PRISM.]
[FYO14] Ling Fang, Yoriyuki Yamagata and Yutaka Oiwa. Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking. In Proc. 3rd International Workshop on Engineering Safety and Security Systems 2014 (ESSS'14), volume 150 of EPTCS, pages 35-49. 2014. [Uses probabilistic model checking and PRISM to analyse resilience strategies for micro processor units.]
[RLK14] Pedro Rodrigues, Emil Lupu and Jeff Kramer. LTSA-PCA: tool support for compositional reliability analysis. In 36th International Conference on Software Engineering, ICSE '14, Companion Proceedings, pages 548-551. 2014. [Presents an extension of the LTSA model checker for compositional reliability analysis, which uses a connection to PRISM. ]
[ZR14] Yang Zhao and Kristin Yvonne Rozier. Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems. In Proc. IEEE/ACM 2014 International Conference on Computer-Aided Design (ICCAD'14), IEEE/ACM. 2014. [bib] [Uses probabilistic model checking and PRISM to study safety properties of automated air traffic control systems.]
[SR14] Guoxin Su and David S. Rosenblum. Perturbation analysis of stochastic systems with empirical distribution parameters. In Proc. 36th International Conference on Software Engineering (ICSE'14). 2014. [Proposes techniques for analysing peturbations in probabilistic models using parametric model checking and a connection to PRISM.]
[Ald14] Alessandro Aldini. Saving Privacy in Trust-Based User-Centric Distributed Systems. In Proc. 8th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE'14), pages 76-81. 2014. [Analyses privacy, cost and trust trade-offs in user-centric distributed systems using PRISM.]
[LJ14] Nian-Ze Lee and Jie-Hong R. Jiang. Towards formal evaluation and verification of probabilistic design. In Proc. 2014 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'14). 2014. [Uses PRISM as part of a framework to verify approximate and probabilistic designs for circuits.]
[GCB14] Efficient Runtime Quantitative Verification using Caching, Lookahead, and Nearly-Optimal Reconfiguration. Simos Gerasimou, Radu Calinescu and Alec Banks.. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), pages 115-124. 2014. [Presents advances in runtime quantitative verification with an implementation that uses PRISM as a model checker.]
[CMG14] Javier Cámara, Gabriel A. Moreno and David Garlan. Stochastic Game Analysis and Latency Awareness for Proactive Self-Adaptation. In Proc. 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'14), pages 155-164, ACM. 2014. [Uses PRISM-games to analyse adaptation tactic latency in self-adaptive systems.]
[BCG14] Ludovica Luisa Vissat, Allan Clark and Stephen Gilmore. Finding optimal timetables for Edinburgh bus routes. In Proc. 7th International Workshop on Practical Applications of Stochastic Modelling (PASM'14). 2014. [Uses various techniques and tools, including PRISM, to analyse and optimise bus reliability.]
[DKSS14] Tushar Deshpande, Panagiotis Katsaros, Scott Smolka and Scott Stoller. Stochastic Game-Based Analysis of the DNS Bandwidth Amplification Attack Using Probabilistic Model Checking. In Proc. 10th European Dependable Computing Conference (EDCC'14). 2014. [Analyses the DNS bandwidth amplification attack using a stochastic game model and PRISM-games.]
[HMST14b] Khaza Anuarul Hoque, Otmane Ait Mohamed, Yvon Savaria and Claude Thibeault. Probabilistic model checking based DAL analysis to optimize a combined TMR-blind-scrubbing mitigation technique for FPGA-based aerospace applications. In Proc. 12th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'14), pages 175-184, IEEE. 2014. [Uses probabilistic model checking and PRISM to analyse soft-error mitigation techniques and associated dependability properties of SRAM-based FPGAs.]
[LMJ+14] Yu Lu, Alice Miller, Chris Johnson, Zhaoguang Peng and Tingdi Zhao. Availability Analysis of Satellite Positioning Systems for Aviation using the PRISM Model Checker. In Proc. 17th IEEE International Conference on Computational Science and Engineering (CSE'14), IEEE. 2014. [Performs availability analysis of satellite positioning systems for aircraft guidance using probabilistic model checking and PRISM.]
[CS14b] Muffy Calder and Michele Sevegnani. Do I need to fix a failed component now, or can I wait until tomorrow?. In Proc. 10th European Dependable Computing Conference (EDCC'14), pages 70-81, IEEE. 2014. [Proposes methods for operational decision making in complex systems using predictive event-based modelling, probabilistic model checking and PRISM.]
[RC14b] José Ignacio Requeno and José Manuel Colom. Timed and Probabilistic Model Checking over Phylogenetic Trees. In 8th International Conference on Practical Applications of Computational Biology & Bioinformatics (PACBB'14), volume 294 of Advances in Intelligent Systems and Computing Volume, pages 105-112, Springer. 2014. [Analyses phylogenetic trees using probabilistic model checking and PRISM.]
[ACHG14] Oana Andrei, Muffy Calder, Matthew Higgs and Mark Girolami. Probabilistic Model Checking of DTMC Models of User Activity Patterns. In Proc. 11th International Conference on Quantitative Evaluation of SysTems (QEST'14), volume 8657 of LNCS, pages 138-153, Springer. 2014. [Analyses user activity patterns modelled as Markov chains using PRISM.]
[MFH+14] Anitha Murugesan, Lu Feng, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael W. Whalen and Insup Lee. Exploring the Twin Peaks using Probabilistic Verification Techniques. In Proc. 4th International Workshop on Twin Peaks of Requirements and Architecture (TwinPeaks'14), ACM. 2014. [Uses probabilistic verification and PRISM as part of an approach to analyse the co-evolution of system requirements and system architecture/design.]
[GTP14] Debjani Ghosh, Mayank Pandey and Neeraj Tyagi. Stochastic Modelling and Analysis of Video on Demand System with VCR Functionalities. In Proc. 2014 International Computer Science and Engineering Conference (ICSEC'14), pages 78-84, IEEE. 2014. [Uses PRISM to analyse quality-of-service properties of a distributed Video on Demand streaming application.]
[FBZ14] João M Franco, Raul Barbosa, Mário Zenha-Rela. Availability Evaluation of Software Architectures through Formal Methods. In Proc. 9th International Conference on the Quality of Information. 2014. [Analyses availability constraints on software architectures, including probabilistic model checking with PRISM.]
[DKB14] Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Probabilistic model checking for energy analysis in software product lines. In Proc. 13th international conference on Modularity (MODULARITY'14), pages 169-180, ACM. 2014. [Proposes a compositional modelling framework for software product lines which makes use of PRISM for analysis of system components.]
[SDC+14] Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry and Sanjit A. Seshia. Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior. In Proc. AAAI Spring Symposium on Formal Verification & Modeling in Human-Machine Systems. 2014. [Analyses formal probabilistic models of driver behaviour, constructed with PRISM.]
[CRJB14] Radu Calinescu, Yasmin Rafiq, Kenneth Johnson and Mehmet Emin Bakir . Adaptive Model Learning for Continual Verification of Non-Functional Properties. In Proc. 5th ACM/SPEC international conference on Performance engineering (ICPE'14), pages 87-98, ACM. 2014. [Proposes adaptive model learning techniques for continuous probabilistic verification, including PRISM as a backend solver.]

2013

[PLSVS13] Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In Proc. 25th International Conference on Computer Aided Verification (CAV'13). 2013. [Develops techniques for verification of MDPs with convex uncertainties, implemented through an interface to PRISM.]
[KJR13] Radu Calinescu, Kenneth Johnson and Yasmin Rafiq. Developing Self-Verifying Service-Based Systems. In Proc. 28th IEEE/ACM International Conference on Automated Software Engineering (ASE'13), IEEE. 2013. [Describes a self-verifying framework for service-based systems, including PRISM as a backend solver.]
[ZREF13] Fokion Zervoudakis, David S. Rosenblum, Sebastian Elbaum and Anthony Finkelstein. Cascading Verification: An Integrated Method for Domain-Specific Model Checking. In Proc. 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE'13), pages 400-410 , ACM. 2013. [Proposes a domain-specific model checking framework, including PRISM as an underlying solver.]
[FBZ13] João Franco, Raul Barbosa and Mário Zenha Rela. Reliability analysis of software architecture evolution. In Proc. Latin-American Symposium on Dependable Computing (LADC'13). 2013. [Analyses quality attributes of software architectures by translating an architecture design language into PRISM. ]
[PLM+13] Zhaoguang Peng, Yu Lu, Alice Miller, Chris Johnson and Tingdi Zhao. A Probabilistic Model Checking Approach to Analysing Reliability, Availability, and Maintainability of a Single Satellite System. In Proc. 7th European Symposium on Computer Modelling and Simulation (EMS'13), pages 611-616. 2013. [Uses probabilistic model checking and PRISM to analyse reliability, availability and maintainability properties of a satellite system.]
[JKG13] Benjamin Johnson and Hadas Kress-Gazit. Analyzing and revising high-level robot behaviors under actuator error. In Proc. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'13), pages 741-748. 2013.
[JCK13] Kenneth Johnson, Radu Calinescu and Shinji Kikuchi. An Incremental Verification Framework for Component-Based Software Systems. In Proc. 16th International ACM Sigsoft symposium on Component-based software engineering (CBSE'13), pages 33-42. 2013. [Presents a framework for the efficient reverification of component-based software system, with a software prototype built on top of PRISM.]
[RBC+13] Neha Rungta, Guillaume Brat, William J. Clancey, Charlotte Linde, Franco Raimondi, Chin Seah and Michael Shafto. Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems. In Proc. International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
[HRRS13] Josie Hunter, Franco Raimondi, Neha Rungta and Richard Stocker. A synergistic and extensible framework for multi-agent system verification. In Proc. International conference on Autonomous Agents and Multi-Agent Systems (AAMAS'13). 2013. [Presents a verification approach based on the Brahms multi-agent framework, with connections to several model checkers, including PRISM.]
[BEK+13] Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Selec. In Proc. NASA Formal Methods Symposium (NFM'13), pages 307-321. 2013. [Verifies the Probabilistic-Write/Copy-Select (PWCS) protocol using PRISM.]
[LFL13] Florian Leitner-Fischer and Stefan Leue. On the Synergy of Probabilistic Causality Computation and Causality Checking. In Proc. 20th International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 246-263, Springer. 2013. [Develops an approach for causality checking, which uses PRISM for some of the underlying computations.]
[CG13] Sagar Chaki and Joseph Andrew Giampapa. Probabilistic Verification of Coordinated Multi-robot Missions. In Proc. 20th International Symposium on Model Checking Software (SPIN'13), volume 7976 of LNCS, pages 135-153, Springer. 2013. [Proposes techniques to verify multi-robot systems, including the use of PRISM.]
[KATH13] Adil Khurram, Haider Ali, Arham Tariq and Osman Hasan. Formal Reliability Analysis of Protective Relays in Power Distribution Systems. In Proc. International Workshop on Formal Methods for Industrial Critical Systems (FMICS'13), pages 169-183, Springer. 2013. [Models and verifies power distribution relays using PRISM.]
[TPTL13] Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna and Linas Laibinis. Formal Development and Quantitative Assessment of a Resilient Multi-robotic System. In Proc. 5th International Workshop on Software Engineering for Resilient Systems (SERENE'13), volume 8166 of LNCS, pages 109-124, Springer. 2013. [Analyses the resilience of a multi-robotic system using Event-B and PRISM.]

2012

[YZN+12] Ender Yüksel, Huibiao Zhu, Hanne Riis Nielson, Heqing Huang and Flemming Nielson. Modelling and Analysis of Smart Grid: A Stochastic Model Checking Case Study. In Proc. 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12), pages 25-32, IEEE. 2012. [Models and verifies a Chinese smart grid implementation using PRISM.]
[BCFCC12] Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos and Sérgio V. A. Campos. A Probabilistic Model Checking Approach to Investigate the Palytoxin Effects on the Na+/K+-ATPase. In Proc. 7th Brazilian Symposium on Bioinformatics (BSB'12). 2012. [Studies the effects of the palytoxin toxin in transmembrane ionic transport systems using various probabilistic model checking tools, including PRISM.]
[TPT+12] Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Timo Latvala and Laura Nummila. Formal Development and Assessment of a Reconfigurable On-board Satellite System. In Proc. International Conference on Computer Safety, Reliability, and Security (SAFECOMP'12), pages 210-222. 2012. [Uses Event-B, in conjunction with PRISM, to verify fault tolerance of satellite systems.]
[LLL+12] Robyn Lutz, Jack Lutz, James Lathrop, Titus Klinge, Eric Henderson, Divita Mathur and Dalia Abo Sheasha. Engineering and Verifying Requirements for Programmable Self-Assembling Nanomachines. In Proc. 34th ACM/IEEE International Conference on Software Engineering (ICSE'12). 2012. [bib] [Proposes validation techniques for programmable DNA self-assemblies, using DNA origami pliers as an example, and applying PRISM for analysis.]
[AB12] Alessandro Aldini and Alessandro Bogliolo. Model Checking of Trust-Based User-Centric Cooperative Networks. In Proc. 4th International Conference on Advances in Future Internet (AFIN'12). 2012.
[LSPM12] Qian Li, Peter Schaffer, Jun Pang and Sjouke Mauw. Comparative Analysis of Clustering Protocols with Probabilistic Model Checking. In Proc. 6th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'12). 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.
[OGLS12] Frank Ortmeier, Matthias Gudemann, Michael Lipaczewski and Simon Struck. Unifying Probabilistic and Traditional Formal Model Based Analysis. In Proc. MBEES. 2012.
[BPBD12] Manuele Brambilla, Carlo Pinciroli, Mauro Birattari and Marco Dorigo. Property-driven Design for Swarm Robotics. In Proc. 11th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'12). 2012. [Uses probabilistic model checking and PRISM as part of a design process for swarm robotics.]
[HYF+12] Kang He, Hongli Yang, Yachao Feng, Yuan Liu and Zongyan Qiu. Performance Analysis of Data Gathering Protocol Using PRISM. In Proc. 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'12), pages 96-105. 2012. [Uses PRISM to analyse the Power Efficient Algorithm for Data Gathering (PEADG) protocol.]
[LJL+12] Lixing Li, Zhi Jin, Ge Li, Liwei Zheng and Qiang Wei . Modeling and Analyzing the Reliability and Cost of Service Composition in the IoT: A Probabilistic Approach. In Proc. 19th IEEE International Conference on Web Services (ICWS'12), pages 584-591 . 2012. [Uses PRISM to analyse compositions of web services.]
[JD12] Yosr Jarraya and Mourad Debbabi. Formal Specification and Probabilistic Verification of SysML Activity Diagrams. In Proc. 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12). 2012. [Presents a framework for probabilistic verification of SysML activity diagrams via a translation to PRISM.]
[PB12] Sophia Petridou and Stylianos Basagiannis. Towards Energy Consumption Evaluation of the SSL Handshake Protocol in Mobile Communications. In Proc. 9th IEEE Annual Conference on Wireless on-demand Networks Systems and Services (IEEE WONS'12). 2012. [Analyses the energy consumption of the SSL handshake protocol using a PRISM CTMC model.]
[BBOM12] Paolo Ballarini, Jalel Ben-Othman and Lynda Mokdad. Quantitative Verification of WiMAX Traffic Shaping Solutions. In Proc. 7th International Symposium on Intelligent System Techniques for Ad hoc and Wireless Sensor Networks (IST-AWSN). 2012. [Uses probabilistic model checking and PRISM to analyse traffic-shaping schemes for the IEEE 802.16 (WiMAX) standard.]
[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 build with PRISM.]
[SSK+12] Emmanouela Stachtiari, Yannis Soupionis, Panagiotis Katsaros, Anakreontas Mentis and Dimitris Gritzalis. Probabilistic model checking of CAPTCHA admission control for DoS resistant anti-SPIT protection. In Proc. 7th International Conference on Critical Information Infrastructures Security (CRITIS'12). 2012. [Studies the effectiveness of admission control policies for DoS-resistanct CAPTCHA schemes using probabilistic model checking and PRISM.]
[LR12] Adalberto Llarena and David Rosenblueth. Model Checking Applied to Humanoid Robotic Soccer. In Advances in Autonomous Robotics, volume 7429 of LNCS, Springer. 2012. [Uses PRISM to synthesise parameters of probabilistic strategies for humanoid robotic football.]
[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.]
[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.]
[KG12] Christian Krause and Holger Giese. Probabilistic Graph Transformation Systems. In Proc. 6th International Conference on Graph Transformations (ICGT'12), pages 311-325. 2012. [Proposes techniques to analyse probabilistic graph transformation systems, using the tools HENSHIN and PRISM.]
[TTL12] Anton Tarasyuk, Elena Troubitsyna and Linas Laibinis. Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In Proc. 9th International Conference on Integrated Formal Methods (IFM'12), pages 237-252. 2012. [Uses PRISM to analyse dynamic service architectures modelled in a probabilistic extension of Event-B.]
[CKJ12] Radu Calinescu, Shinji Kikuchi and Kenneth Johnson. Compositional Reverification of Probabilistic Safety Properties for Large-Scale Complex IT Systems. In Proc. 17th Monterey Workshop on Development, Operation and Management of Large-Scale Complex IT Systems. 2012. [Uses PRISM and its compositional (assume-guarantee) extensions to analyse large-scale complex IT systems (LSCITS).]
[LLL+12b] Robyn Lutz, Jack Lutz, James Lathrop, Titus Klinge, Divita Mathur, D. M. Stull, Taylor Bergquist and Eric Henderson. Requirements Analysis for a Product Family of DNA Nanodevices. In Proc. 20th IEEE International Requirements Engineering Conference. 2012. [Applies requirements engineering methods to DNA nanodevices and uses PRISM to verify the generated properties.]
[AASB12] Zaid Al-bayati, O. Ait Mohamed, Yvon Savaria and Mounir Boukadoum. Probabilistic model checking of clock domain crossing interfaces. In Proc. IEEE 10th International New Circuits and Systems Conference (NEWCAS'12). 2012. [Uses PRISM to verify clock domain crossing (CDC) protocols.]
[VK12] Mahsa Varshosaz and Ramtin Khosravi. Modeling and Verification of Probabilistic Actor Systems Using pRebeca. In Proc. 14th International Conference on Formal Engineering Methods, Formal Methods and Software Engineering (ICFEM'12), volume 7635 of LNCS, Springer. 2012. [Uses PRISM to analyse systems described in a probabilistic actor-based modelling language called pRebeca.]
[HS12] Luke Herbert and Robin Sharp. Using stochastic model checking to provision complex business services. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 98-105, IEEE. 2012. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows. Illustrated on a medical case study.]
[LSO12] Michael Lipaczewski, Simon Struck and Frank Ortmeier. Using Tool-Supported Model Based Safety Analysis - Progress and Experiences in SAML Development. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 159-166. 2012. [Presents tool support for the safety analysis modelling language (SAML), which connects to PRISM for probabilistic verification.]
[SLOG12] Simon Struck, Michael Lipaczewski, Frank Ortmeier and Matthias Güdemann. Multi-objective Optimization of Formal Specifications. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 201-208. 2012. [Develops model-based optimisation methods which connect to PRISM for model analysis.]
[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.]
[FBZ12] Joao M. Franco, Raul Barbosa and Mario Zenha-Rela. Automated Reliability Prediction from Formal Architectural Descriptions. In Proc. 2012 Joint Working IEEE/IFIP Conference on Software Architecture (WICSA) and European Conference on Software Architecture (ECSA). 2012. [Analyses quality attributes of software architectures by translating an architecture design language into PRISM.]

2011

[PBP11] Ioannis Paparrizos, Stylianos Basagiannis and Sophia Petridou. Quantitative Analysis for Authentication of Low-cost RFID Tags. In Proc. 36th IEEE Conference on Local Computer Networks (LCN'11), IEEE. 2011. [Analyses the computation and transmission costs of RFID tags using a PRISM DTMC model.]
[TNBB11] Amir Tavala, Soroosh Nazema and Ali A. Babaei-Brojeny. Verification of Quantum Protocols with a Probabilistic Model-Checker. In Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008), volume 270 of ENTCS, pages 175-182. 2011. [bib]
[LFL11] Florian Leitner-Fischer and Stefan Leue. QuantUM: Quantitative Safety Analysis of UML Models. In Proc. 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11). 2011. [bib]
[CDLPB11] Igor Cizelj, Xu Chu Ding, Morteza Lahijanian, Alessandro Pinto and Calin Belta. Probabilistically Safe Vehicle Control in a Hostile Environment. In Proc. 18th World Congress of the International Federation of Automatic Control (IFAC). 2011. [bib] http://hyness.bu.edu/calin/Publications.html
[YPM+11] Qixia Yuan, Jun Pang, Sjouke Mauw, Panuwat Trairatphisan, Monique Wiesinger and Thomas Sauter. A Study of the PDGF Signaling Pathway with PRISM. In Proc. 3rd International Workshop on Computational Models for Cell Processes (COMPMOD'11), volume 68 of EPTCS, pages 65-81. 2011.
[LMP11] Pietro Liò, Emanuela Merelli and Nicola Paoletti. Multiple verification in computational modeling of bone pathologies. In Proc. 3rd International Workshop on Computational Models for Cell Processes (COMPMOD'11), volume 68 of EPTCS, pages 82-96. 2011. [bib]
[KG11] Christian Krause and Holger Giese. Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements. In Proc. 13th International Workshop on Verification of Infinite-State Systems (INFINITY'11). 2011. [bib]
[LMG11] Markus Lumpe, Indika Meedeniya and Lars Grunske. PSPWizard: Machine-assisted definition of temporal logical properties with specification patterns. In Proc. 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering and 13rd European Software Engineering Conference (ESEC/FSE'11), pages 468-471. 2011. [bib]
[FGHM11] V. Fern'ández, M.-J. Garc'ia-Mart'inez, L. Hern'andez-Encinas and A. Marti'in. Formal Verification of the Security of a Free-Space Quantum Key Distribution System. In Proc. 2011 World Congress in Computer Science, Computer Engineering, and Applied Computing (WORLDCOMP'11), 2011 International Conference on Security and Management (SAM'11). 2011. [bib]
[TK11] Li Tan and Axel Krings. An Adaptive N-variant Software Architecture for Multi-Core Platforms: Models and Performance Analysis. In Proc. International Conference on Computational Science and Its Applications, Part II (ICCSA'11), pages 490-505. 2011. [bib]
[CDGFS11] J. Clement, C. Delporte-Gallet, H. Fauconnie and M. Sighireanu. Guidelines for the Verification of Population Protocols. In Proc. 31st International Conference on Distributed Computing Systems (ICDCS'11). 2011. [bib]
[DKBS11] Tushar Deshpande, Panagiotis Katsaros, Stylianos Basagiannis and Scott Smolka. Formal Analysis of the DNS Bandwidth Amplification Attack and Its Countermeasures Using Probabilistic Model Checking. In Proc. 13th IEEE International Symposium on High-Assurance Systems Engineering (HASE'11), pages 360-367. 2011. [bib]
[KLV11] Jayanand Asok Kumar, Lingyi Liu and Shobha Vasudevan. Scaling Probabilistic Timing Verification of Hardware Using Abstractions in Design Source Code. In Proc. 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD'11). 2011. [bib]
[JRC11] Kenneth Johnson, Simon Reed and Radu Calinescu. Specification and Quantitative Analysis of Probabilistic Cloud Deployment Patterns. In Proc. 7th Haifa Verification Conference (HVC'11). 2011. [bib]
[AB11] R. Abo and K. Barkaoui. A performability analysis of mobile wireless sensor networks with probabilistic model checking. In Proc. Wireless Advanced (WiAd'11), pages 283-288. 2011.
[MST11a] Tamara Mendt, Carsten Sinz and Olga Tveretina. Probabilistic Model Checking of Constraints in a Supply Chain Business Process. In Business Information Systems, volume 87 of Lecture Notes in Business Information Processing, pages 1-12. 2011.
[KSB+11] Heiko Koziolek, Bastian Schlich, Carlos Bilich, Roland Weiss, Steffen Becker, Klaus Krogmann, Mircea Trifu, Raffaela Mirandola and Anne Martens. An Industrial Case Study on Quality Impact Prediction for Evolving Service-Oriented Software. In Proc. 33rd ACM/IEEE International Conference on Software Engineering (ICSE'11), pages 776-785, ACM. 2011.
[GO11] Matthias Gudemann and Frank Ortmeier. Towards Model-driven Safety Analysis. In Proc. 3rd International Workshop on Dependable Control of Discrete Systems (DCDS'11). 2011.
[KLFL11] Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue. From Probabilistic Counterexamples via Causality to Fault Trees. In Proc. 30th International Conference on Computer Safety, Reliability, and Security (SAFECOMP'11). 2011.
[KF11] Savas Konur and Michael Fisher. Formal Analysis of a VANET Congestion Control Protocol through Probabilistic Verification. In Proc. 73rd IEEE Vehicular Technology Conference (VTC'11). 2011.
[DYL+11] Chen Deng, Hongli Yang, Husheng Liao, Meng Sun and Zongyan Qiu. Analysis of WS-BPEL Processes in PRISM. In 199-202, pages Proc. 5th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'11). 2011. [Uses PRISM to analyse processes specified in the Web Services Business Process Execution Language (WS-BPEL). ]
[PBA+11] Sophia Petridou, Stylianos Basagiannis, Nikolaos Alexiou, Georgios Papadimitriou and Panagiotis Katsaros. Quantitative Model Checking of an RSA-based Email Protocol on Mobile Devices. In Proc. 16th IEEE Symposium on Computers and Communications (ISCC'11). 2011. [bib] [Analyses the Certified E-mail Message Delivery (CEMD) protocol using PRISM.]
[KM11] Shinji Kikuchi, Yasuhide Matsumoto. Performance Modeling of Concurrent Live Migration Operations in Cloud Computing Systems using PRISM Probabilistic Model Checker. In Proc. 4th International Conference on Cloud Computing (IEEE Cloud 2011). July 2011. [bib]

2010

[GO10] Matthias Gudemann and Frank Ortmeier. Probabilistic Model-Based Safety Analysis. In Proc. Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010). 2010.
[GPM10] X. Ge, R. Paige and J. McDermid. Analysing System Failure Behaviours With PRISM. In Proc. 4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, pages 130-136. 2010. [bib]
[ABK+10] N. Alexiou, S. Basagiannis, P. Katsaros, T. Dashpande and S. Smolka. Formal Analysis of the Kaminsky DNS Cache-Poisoning Attack Using Probabilistic Model Checking. In Proc. IEEE 12th International Symposium on High-Assurance Systems Engineering (HASE'10), pages 94-103. 2010. [bib] http://www.cs.sunysb.edu/~sas/kaminsky/
[KV10] J. A. Kumar and S. Vasudevan. Statistical guarantees of performance for MIMO designs. In Proc. IEEE/IFIP International Conference on Dependable Systems & Networks (DSN'10). 2010. [bib]
[KV10b] J. A. Kumar and S. Vasudevan. Automatic compositional reasoning for probabilistic model checking of hardware designs. In Proc. 7th International Conference on Quantitative Evaluation of SysTems (QEST'10), IEEE CS Press. 2010. [bib]
[STK+10] D. Schumm, O. Turetken, N. Kokash, A. Elgammal, F. Leymann and W.-J. van den Heuvel. Business Process Compliance through Reusable Units of Compliant Processes. In Proc. 10th International Conference on Current Trends in Web Engineering (ICWE'10). 2010. [bib]
[KH10] K. Kobayashi and K. Hiraishi. Reachability analysis of probabilistic Boolean networks using model checking. In Proc. SICE Annual Conference 2010, pages 829-832. 2010. [bib]
[RAFL10] G. N. Rodrigues, V. Alves, R. Franklin and L. Laranjeira. Dependability Analysis in the Ambient Assisted Living Domain: an Exploratory Case Study. In Proc. 4th Brazilian Symposium on Software Components, Architectures and Reuse, pages 150-159. 2010. [bib]
[YZH+10] Hongli Yang, Liang Zhou, Kang He, Chen Deng, Xiangpeng Zhao and Zongyan Qiu. A probabilistic QoS model-checking for dynamic routing protocol. In Proc. 10th International Conference on Quality Software (QSIC'10), pages 441-448, IEEE. 2010. [bib]
[AA10] M. Akbarzadeh and M. Azgomi. A framework for probabilistic model checking of security protocols using coloured stochastic activity networks and PDETool. In Proc. 5th International Symposium on Telecommunications (IST'10), pages 210-215. 2010. [bib]
[OGS10] P. Oliveira, R. Gomes and M. Song. Large Scale Genetic Identity Inference Using Probabilistic Model Checking. In 2010 IEEE International Conference on Systems Man and Cybernetics (SMC'10), pages 3508-3512, IEEE. 2010. [bib]
[HGB+10] Ru He, Paul Jennings, Samik Basu, Arka Ghosh and Huaiqing Wu. A bounded statistical approach for model checking of unbounded until properties. In 25th IEEE/ACM International Conference on Automated Software Engineering (ASE'10), pages 225-234. 2010. [bib]
[LWAB10] M. Lahijanian, J. Wasniewski, S. B. Andersson and C. Belta. Motion Planning and Control from Temporal Logic Specifications with Probabilistic Satisfaction Guarantees. In Proc. 2010 IEEE International Conference on Robotics and Automation, pages 3227-3232. 2010. [bib] http://hyness.bu.edu/calin/Publications.html
[KSB10] Heiko Koziolek, Bastian Schlich and Carlos Bilich. A Large-Scale Industrial Case Study on Architecture-based Software Reliability Analysis. In Proc. IEEE 21st International Symposium on Software Reliability Engineering (ISSRE'10), pages 279-288. 2010. [bib]
[HKL+10] B. Haverkort, M. Kuntz, F. Leitner-Fischer, A. Remke and S. Roolvink. Probabilistic Verification of Architectural Software Models using SoftArc and Prism. In Proc. ESREL Annual Conference. 2010. [bib]
[BESW10] Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski and Anton Wijs. GPU-PRISM: An Extension of PRISM for General Purpose Graphics Processing Units. In Proc. 9th International Workshop on Parallel and Distributed Methods in Verification. 2010. [bib]
[HWHY10] Wei Huang, Gengyu Wei, Nan Hu and Yixian Yang. Design and Analysis of Heartbeat Protocol in NIDS Cluster. In Proc. 2nd International Conference on Future Computer and Communication (ICFCC'10). 2010.
[GO10b] Matthias Gudemann and Frank Ortmeier. A Framework for Qualitative and Quantitative Formal Model-Based Safety Analysis. In Proc. 12th IEEE High Assurance Systems Engineering Symposium (HASE'10), pages 132-141. 2010.
[KDF10] Savas Konur, Clare Dixon and Michael Fisher. Formal Verification of Probabilistic Swarm Behaviours. In Proc. 7th International Conference on Swarm Intelligence (ANTS'10), volume 6234 of LNCS, pages 440-447, Springer. 2010. [bib]
[BMA10] Cristiano Bertolini, Alexandre Mota and Eduardo Aranha. Calibrating Probabilistic GUI Testing Models Based on Experiments and Survival Analysis. In Proc. 21st IEEE International Symposium on Software Reliability Engineering (ISSRE'10), pages 319-328. 2010. [Uses PRISM to evaluate software testing techniques for graphical user interfaces.]
[GMS+10] Adriano Gomes, Alexandre Mota, Augusto Sampaio, Felipe Ferri and Julio Buzzi. Systematic Model-Based Safety Assessment Via Probabilistic Model Checking. In 4th International Symposium on Leveraging Applications on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'10), pages 625-639, Springer. 2010. [Uses PRISM for quantitative safety assessment, with a case study of an actuator control system.]
[YK10] Haidi Yue and Joost-Pieter Katoen. Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption. In Proc. 17th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA'10) , volume 6148 of LNCS, pages 247–261, Springer. 2010. [Analyses a randomised leader election protocol using PRISM.]

2009

[BM09] Cristiano Bertolini and Alexandre Mota. Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. In Proc. 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09). 2009. [bib] http://www.cin.ufpe.br/~cb2/ [Uses PRISM to evaluate software testing techniques for graphical user interfaces.]
[BMM09] Paolo Ballarini, Radu Mardare and Ivan Mura. Analysing Biochemical Oscillation through Probabilistic Model Checking. In Proc. 2nd Workshop From Biology to Concurrency and Back (FBTC'08), volume 229 (issue 1) of Electronic Notes in Theoretical Computer Science, pages 3-19, Elsevier. 2009. [bib]
[ACvdM+09] F. Arbab, T. Chothia, R. van der Mei, M. Sun, Y.-J. Moon and C. Verhoef. From Coordination to Stochastic Models of QoS. In Proc. 11th international conference on Coordination Models and Languages (Coordination'09). 2009. [bib]
[BES09] D. Bosnacki and S. Edelkamp and D. Sulewski. Efficient Probabilistic Model Checking on General Purpose Graphics Processors. In C. Pasareanu (editor), Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 32-49, Springer. 2009. [bib]
[MKUM09] Paulo Maia, Jeff Kramer, Sebastián Uchitel and Nabor Mendonça. Towards accurate probabilistic models using state refinement. In Proc. 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/SIGSOFT FSE'09), pages 281-284. 2009. [Presents state refinement techniques for generating accurate probabilistic models which are analysed using PRISM.]
[BLMS09] R. Barbuti, F. Levi, P. Milazzo and G. Scatena. Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates. In 3rd International Workshop on Reachability Problems (RP'09). 2009. [bib]
[BW09] B. Beckert and M. Wagner. Probabilistic Models for the Verification of Human-Computer Interaction. In Proc. 32nd Annual German Conference on Artificial Intelligence. 2009. [bib]
[BGK+09] T. Berczes, G. Guta, G. Kusper, W. Schreiner and J. Sztrik. Analyzing a Proxy Cache Server Performance Model with the Probabilistic Model Checker PRISM. In Proc. 5th International Workshop on Automated Specification and Verification of Web Systems (WWV'09). 2009. [bib]
[AFG+09] H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner and S. Leue. Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). 2009. [bib]
[BF09] R. Bakhshi and A. Fehnker. On the impact of modelling choices for distributed information spread. A comparative study. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). 2009. [bib]
[MS09] J. Misra and I. Saha. A Reinforcement Model for Collaborative Security and Its Formal Analysis. In Proc. New Security Paradigms Workshop (NSPW'09). 2009. [bib] [Proposes a reinforcement framework for collaborative monitoring of security violations and anlayses it using PRISM.]
[HHZ09] E. Hahn, H. Hermanns and L. Zhang. Probabilistic Reachability for Parametric Markov Models. In C. Pasareanu (editor), Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 88-106, Springer. 2009. [bib]
[SM09] I. Saha and D. Mukhopadhyay. Quantitative Analysis of a Probabilistic Non-repudiation Protocol through Model Checking. In Proc. 5th International Conference on Information Systems Security (ICISS'09), volume 5905 of LNCS, pages 292-300, Springer. 2009. [bib]
[DTC+09] A. Dhama, O. Theel, P. Crouzen, H. Hermanns, R. Wimmer and B. Becker. Dependability Engineering of Silent Self-stabilizing Systems. In Proc. 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems, volume 5873 of LNCS, pages 238-253, Springer. 2009. [bib]
[Ndu09] U. Ndukwu. Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems. In Proc. Workshop on Quantitative Formal Methods (QFM'09). 2009. [bib]
[CV09] M. Casadei and M. Viroli. Using probabilistic model checking and simulation for designing self-organizing systems. In Proc. ACM Symposium on Applied Computing (SAC'2009), pages 2103-2104. 2009. [bib]
[JM09] L. Jagadeesan and V. Mendiratta. Voice Communication Mashups: Formal Specification and Composition of Service Level Agreements. In 3rd International Conference on Next Generation Mobile Applications, Services and Technologies (NGMAST'09). 2009. [bib]
[BGH09] A. Basu, A. Ghosh and R. He. Approximate Probabilistic Model Checking Using Bounded Until Properties. In Proc. 11th International Conference on Formal Engineering Methods (ICFEM'09),. 2009. [bib]
[MDT09] Nils Mullner, Abhishek Dhama and Oliver Theel. Deriving a Good Trade-off Between System Availability and Time Redundancy. In Proc. Symposia and Workshops on Ubiquitous, Autonomic and Trusted Computing (UIC-ATC'09), IEEE. 2009. [Studies design trade-offs in self-stabilising systems using several methods, including probabilistic model checking with PRISM.]
[HH09] A. Hartmanns and H. Hermanns. A Modest Approach to Checking Probabilistic Timed Automata. In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). To appear. September 2009. [bib]
[AMMKQ09] F. Arbab, S. Meng, Y.-J. Moon, M. Kwiatkowska and H. Qu. Reo2MC: a Tool Chain for Performance Analysis of Coordination Models. In Hans van Vliet, Valérie Issarny (editor), The 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 287-288, ACM. August 2009. [pdf] [bib] [Presents a tool chain for analysing Stochastic Reo models, incorporating PRISM.]
[Dwo09] H. Dworak. The Design and Implementation of a Documentation Generator for the PRISM Language. In Proc. 4th International Conference on Dependability of Computer Systems (DepCoS-RELCOMEX'09), pages 91-98, IEEE Computer Society. June 2009. [bib] http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=5261015

2008

[Tan08] Li Tan. Model check stochastic supply chains. In Proc. IEEE International Conference on Information Reuse and Integration (IRI'08), pages 416 - 421. 2008.
[AGM08] D. Ardagna, C. Ghezzi and R. Mirandola. Model Driven QoS Analyses of Composed Web Services. In Proc. ServiceWave 2008, volume 5377 of LNCS, pages 299-311, Springer. 2008. [bib]
[GGMT08] S. Gallotti, C. Ghezzi, R. Mirandola and G. Tamburrelli. Quality Prediction of Service Compositions through Probabilistic Model Checking. In Proc. 4th International Conference on the Quality of Software-Architectures (QoSA'08), volume 5281 of LNCS, pages 119-134, Springer. 2008. [bib]
[BKPA08] S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou. A Probabilistic Attacker Model for Quantitative Verification of DoS Security Threats. In Proc. 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'08), pages 12-19, IEEE CS Press. 2008. [bib] http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=4591503&arnumber=4591526&count=285&index=22
[CGGH08] F. Ciocchetta, S. Gilmore, M. L. Guerriero and J. Hillston. Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems. In Proc. 3rd International Workshop on Practical Applications of Stochastic Modelling (PASM'08), volume 232 of ENTCS, pages 17-38. 2008. [bib]
[CT08] A. Coker and V. Taylor. Performance and Reliability Analysis of a Scaled Multi-Switch Junction Crossbar Nanomemory and Demultiplexer. In Proc. IEEE NANO Conference. 2008. [bib] http://prophesy.cs.tamu.edu/publications.html
[WS08] F. Werner and P. Schmitt. Analysis of the Authenticated Query Flooding Protocol by Probabilistic Means. In Proc. 5th Annual Conference on Wireless On demand Network Systems and Services (WONS'08), pages 101-104. 2008. [bib] http://ieeexplore.ieee.org/xpl/tocresult.jsp?isnumber=4459341&isYear=2008
[BPdV08] D. Bosnacki, T. Pronk and E. de Vink. In Silico Modelling and Analysis of Ribosome Kinetics and aa-tRNA Competition. In R.-J. Back and I. Petre (editors), Proc. Workshop on Computational Models for Cell Processes (COMPMOD'08), pages 23-38. 2008. [bib] http://www.win.tue.nl/~evink/research/publications.html
[SAA+08] A. Susu, A. Acquaviva, A. Atienza and and A. De Micheli. Stochastic Modeling and Analysis for Environmentally Powered Wireless Sensor Nodes. In Proc. 6th International Symposium on Modeling and Optimization in Mobile, Ad Hoc, and Wireless Networks (WiOPT'08), pages 11-20. 2008. [bib] http://lsi.epfl.ch/page13139.html
[ZHHW08] L. Zhang, H. Hermanns, E. M. Hahn and B. Wachter. Time-bounded model checking of infinite-state continuous-time Markov chains. In Proc. 8th International Conference on Application of Concurrency to System Design (ACSD'08), pages 98-107. 2008. [bib]
[OTGT08] N. Owens, J. Timmis, A. Greensted and A. Tyrrell. Modelling the Tunability of Early T Cell Signalling Events. In 7th International Conference on Artificial Immune Systems (ICARIS'08), pages 12-23. 2008. [bib]
[HGD08] M. Heiner, D. Gilbert and R. Donaldson. Petri Nets for Systems and Synthetic Biology. In Formal Methods for Computational Systems Biology, volume 5016 of LNCS, pages 215-264, Springer. 2008. [bib]
[CH09] F. Ciocchetta and J. Hillston. Bio-PEPA for epidemiological models. In Proc. 4th International Workshop on Practical Applications of Stochastic Modelling (PASM'09). 2008. [bib]
[IZ08] S. Islam and M. Zaid. Probabilistic analysis of the ASW protocol using PRISM. In IEEE Southeastcon 2008, pages 159-164. 2008. [bib]
[VD08] Bogdan Vukobratović and Stanisa Dautović. Probabilistic Model Checking of Resistive Electrical Circuits. In Proc. 16th Telecommunications Forum (TELFOR'08), pages 508-511. 2008. [bib]
[GRV08] Uwe Glässer, Sarah Rastkar and Mona Vajihollahi.. Modeling and Validation of Aviation Security. In Intelligence and Security Informatics, pages 337-355. 2008. [bib]
[ENT08] J. Elmqvist and S. Nadjm-Tehrani. Formal Support for Quantitative Analysis of Residual Risks in Safety-Critical Systems. In Proc. High Assurance Systems Engineering Symposium (HASE'08). December 2008. [bib] http://www.ida.liu.se/~rtslab/publications/publications.shtml

2007

[GHL07] D. Gilbert, M. Heiner and S. Lehrack. A Unifying Framework for Modelling and Analysing Biochemical Pathways Using Petri Nets. In Proc. 5th International Conference on Computational Methods in Systems Biology (CMSB'07), pages 200-216, Springer. 2007. [bib]
[BGRC+07] F. Bernardini, M. Gheorghe, F. Romero-Campero and N. Walkinshaw. A Hybrid Approach to Modelling Biological Systems. In Proc. 8th Workshop on Membrane Computing, volume 4860 of Lecture Notes in Computer Science, Springer. 2007. [bib] http://www.dcs.shef.ac.uk/~nw/Publications.html
[JSDH07] Yosr Jarraya, Andrei Soeanu, Mourad Debbabi and Fawzi Hassaine. Automatic Verification and Performance Analysis of Time-Constrained SysML Activity Diagrams. In Proc. 14th Annual IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'07), pages 515-522, IEEE. 2007. [bib]
[ABS+07] A. Abate, Y. Bai, N. Sznajder, C. Talcott and A. Tiwari. Quantitative and Probabilistic Modeling in Pathway Logic. In Proc. 7th IEEE International Conference on Bioinformatics and Bioengineering (BIBE'07). 2007. [bib]
[CGW07] R. Colvin, L. Grunske and K. Winter. Probabilistic Timed Behavior Trees. In Proc. 6th International Conference on Integrated Formal Methods (IFM'07). 2007. [bib] http://www.itee.uq.edu.au/~grunske/Research/
[HBGS07] F. He, L. Baresi, C. Ghezzi and P. Spoletini. Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata. In Proc. Formal Techniques for Networked and Distributed Systems (FORTE'07), volume 4574 of Lecture Notes in Computer Science, pages 247-262, Springer. 2007. [bib] http://www.springerlink.com/content/h0438p764643727u/
[STKT07] Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno and Koichi Takahashi. Analyzing the One Dimensional Ising Model by Probabilistic Model Checking. In Proc. IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007). October 2007.
[GCW07] L. Grunske, R. Colvin and K. Winter. Probabilistic Model-Checking Support for FMEA. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07). September 2007. [bib] http://www.itee.uq.edu.au/~kirsten/
[LJ07] C. Langmead and S. Jha. Predicting Protein Folding Kinetics Via Temporal Logic Model Checking. In 7th International Workshop on Algorithms in Bioinformatics (WABI'07), volume 4645 of Lecture Notes in Computer Science, pages 252-264, Springer. September 2007. [bib]
[RSPV07] V. Rosset, P. Souto, P. Portugal and F. Vasques. A Reliability Evaluation of a Group Membership Protocol. In Proc. SAFECOMP 2007, volume 4680 of LNCS, pages 397-410, Springer. September 2007. [bib]
[WZH07] B. Wachter, L. Zhang and H. Hermanns. Probabilistic Model Checking Modulo Theories. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07). September 2007. [bib]
[PVBB07] T. Pronk, E. de Vink, D. Bosnacki and T. Breit. Stochastic Modeling of Codon Bias with PRISM. In I. Linden and C. Talcott (editors), Proc. MTCoord 2007, Paphos, Computer Science Department, University of Cyprus, Nicosia. June 2007. [bib] http://www.liacs.nl/~devink/research/publications.html
[GF07a] J. Greifeneder and J. Frey. Probabilistic Timed Automata for Modeling Networked Automation Systems. In Proc. 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS), pages 143-148. June 2007. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[Der07] S. Derisavi. A Symbolic Algorithm for Optimal Markov Chain Lumping. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 139-154, Springer. March 2007. [bib] http://www.sce.carleton.ca/~derisavi/publications/index.html

2006

[McI06] A. McIver. Quantitative refinement and model checking for the analysis of probabilistic systems. In Proc. Formal Methods (FM'06). To appear. 2006. [bib]
[CDDS06] D. Cerotti, D. D'Aprile, S. Donatelli and J. Sproston. Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools. In Proc. 6th International Conference on Application of Concurrency to System Design (ACSD'06), IEEE Computer Society Press. 2006. [bib]
[BM06] Paolo Ballarini and Alice Miller. Model Checking Medium Access Control for Sensor Networks. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods (ISoLA'06), pages 255-262. 2006. [Uses PRISM to verify S-MAC, a medium access control protocol for wireless sensor networks.]
[MF06] Annabelle McIver and Ansgar Fehnker. Formal Techniques for the Analysis of Wireless Networks. In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'06), pages 263–270. 2006. [Applies various formal verification techniques to wireless networks, including probabilistic model checking with PRISM.]
[RCGB+06] Francisco José Romero-Campero, Marian Gheorghe, Luca Bianco, Dario Pescini, Mario J. Péerez-Jiménez and Rodica Ceterchi. Towards Probabilistic Model Checking on P Systems Using PRISM. In Workshop on Membrane Computing, pages 477-495. 2006.
[BFW06b] Paolo Ballarini, Michael Fisher and Michael Wooldridge. Uncertain Agent Verification through Probabilistic Model-Checking. In Proc. 3rd International Workshop on Safety and Security in Multi-agent Systems (SASEMAS'06). 2006. [bib]
[FG06] A. Fehnker and P. Gao. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In Proc. 5th International Conference on Ad-Hoc, Mobile, and Wireless Networks (ADHOC-NOW'06), volume 4104 of LNCS, pages 128-141, Springer. 2006. [bib] http://www.cse.unsw.edu.au/~ansgar/
[DM06] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Model Checking using Generic Representatives. In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of LNCS, pages 9-23, Springer. October 2006. [bib] http://www.dcs.gla.ac.uk/people/personal/alice/publications.html
[GF06c] J. Greifeneder and J. Frey. Optimizing Quality of Control in Networked Automation Systems using Probabilistic Models. In Proc. 11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'06), pages 372-379. September 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GF06d] J. Greifeneder and J. Frey. Probabilistic Hybrid Automata with Variable Step Width Applied to the Analysis of Networked Automation Systems. In Proc. 3rd IFAC Workshop on Discrete Event System Design (DESDes'06), pages 283-288. September 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GF06b] J. Greifeneder and G. Frey. Determination of Delay Times in Failure Afflicted Networked Automation Systems using Probabilistic Model Checking. In Proc. 6th IEEE International Workshop on Factory Communication Systems (WFCS'06), pages 263-272. June 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GF06] J. Greifeneder and G. Frey. Dependability analysis of networked automation systems by probabilistic delay time analysis. In Proc. 12th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'06), pages 269-274. May 2006. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[GRV06] U. Glasser, S. Rastkar and M. Vajihollahi. Computational Modeling and Experimental Validation of Aviation Security Procedures. In Proc. Intelligence and Security Informatics (ISI'06) . May 2006. http://fas.sfu.ca/pub/cs/techreports/2006/CMPT2006-02.pdf
[ZH06] M. Zhang and D. Van Hung. Formal Analysis of Streaming Downloading Protocol for System Upgrading. In Proc. 4th Workshop on Quantitative Aspects of Programming Languages (QAPL 06). Also available as UNU-IIST Report No. 332. April 2006. [bib] http://www.iist.unu.edu/~dvh/publications_2.html
[BCS+06] D. Bhaduri, S. Shukla, D. Coker, V. Taylor, P. Graham and M. Gokhale. A Hybrid Framework for Design and Analysis of Fault Tolerant Architectures and its Applications to Nanoscale Molecular Crossbar Memories. In Proc. Design, Automation and Test in Europe (DATE'06). March 2006. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html
[BFW06] Paolo Ballarini, Michael Fisher and Michael Wooldridge. Automated Game Analysis via Probabilistic Model Checking: A Case Study. In Proc. 3rd Workshop on Model Checking and Artificial Intelligence (MoChArt'05), volume 149 of ENTCS, pages 125-137, Elsevier. February 2006. [bib] http://www.csc.liv.ac.uk/~mjw/pubs/

2005

[GB05] N. Geisweiller and J. Bonte. Performance Evaluation of a Real-time Simulation Architecture using Probabilistic Model Checking. In Proc. Workshop on Structural Operational Semantics (SOS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 3-24. 2005. [bib] http://linkinghub.elsevier.com/retrieve/pii/S1571066105001854
[Che05] L. Cheung. Randomized Wait-Free Consensus using An Atomicity Assumption. In Proc. 9th International Conference on Principles of Distributed Systems (OPODIS'05). Full version available as Technical Report ICIS-R05035, Institute for Computing and Information Sciences, Radboud University Nijmegen. November 2005. [bib] http://theory.csail.mit.edu/~lcheung/
[Hec05] R. Heckel. Stochastic Analysis of Graph Transformation Systems: A Case Study in P2P Networks. In Proc. 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC'05), volume 3722 of LNCS, Springer. October 2005. http://www.cs.le.ac.uk/people/rh122/papers/2005/Hec05ICTAC.pdf
[GF05] J. Greifeneder and G. Frey. Probabilistic Delay Time Analysis in Networked Automation Systems. In Proc. 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'05), pages 1065-1068. September 2005. [bib] http://www.eit.uni-kl.de/frey/en/people/Juergen/Publics/papers.html
[Bal05] Paolo Ballarini. Automated Game Analysis via Probabilistic Model Checking. In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS'05), pages 15-18. September 2005. [bib] http://www.csc.liv.ac.uk/~paolo/
[DPP05] Y. Deng, C. Palamidessi and J. Pang. Weak Probabilistic Anonymity. In Proc. 3rd International Workshop on Security Issues in Concurrency (SecCo'05). August 2005. [bib] http://www.lix.polytechnique.fr/~catuscia/papers/Anonymity/report_wa.pdf
[BP05] M. Bhargava and C. Palamidessi. Probabilistic Anonymity. In Proc. 16th International Conference on Concurrency Theory (CONCUR'05). August 2005. [bib] http://www.lix.polytechnique.fr/~catuscia/papers/Anonymity/report.pdf
[You05] H. Younes. Ymer: A Statistical Model Checker. In Proc. 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 429-433, Springer-Verlag. July 2005. [bib] http://sweden.autonomy.ri.cmu.edu/papers/
[DM05] A. Donaldson and A. Miller. Symmetry Reduction for Probabilistic Systems. In Proc. 12th workshop on Automated Reasoning, pages 17-18. July 2005. [bib] http://www.dcs.gla.ac.uk/people/personal/alice/publications.html
[BML05b] M. ter Beek, M. Massink and D. Latella. Towards Model Checking Stochastic Aspects of the thinkteam User Interface. In M. Harrison (editor), Proc. 12th International Workshop on Design, Specification and Verification of Interactive Systems (DSVIS'05), volume 3941 of Lecture Notes in Computer Science, pages 39-50, Springer. July 2005. [bib] http://fmt.isti.cnr.it/~mtbeek/
[RG05] A. Roy and K. Gopinath. Improved Probabilistic Models for 802.11 Protocol Verification. In Proc. 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 239-252, Springer-Verlag. July 2005. [bib]
[CKKP05] L. Cloth, J.-P. Katoen, M. Khattri and R. Pulungan. Model checking Markov reward models with impulse rewards. In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 722-731, IEEE CS Press. June 2005. [bib]
[NPBG05] R. Nagarajan, N. Papanikolaou, G. Bowen and S. Gay. An Automated Analysis of the Security of Quantum Key Distribution. In Proc. 3rd International Workshop on Security Issues in Concurrency (SecCo'05). 2005. [bib] http://www.dcs.warwick.ac.uk/~nikos/
[CVGO05] M. Calder, V. Vyshemirsky, D. Gilbert and R. Orton. Analysis of signalling pathways using the PRISM model checker. In Proc. Computational Methods in Systems Biology (CMSB'05), pages 179-190. 2005. [bib] http://www.dcs.gla.ac.uk/~muffy/papers.html

2004

[KSW04a] M. Kuntz, M. Siegle and E. Werner. Symbolic Performance and Dependability Evaluation with the Tool CASPA. In Proc. 1st European Performance Engineering Workshop (EPEW'04), FORTE'04 workshop, volume 3236 of LNCS, pages 293-307, Springer-Verlag. 2004. [bib] http://fakinf.informatik.unibw-muenchen.de/~msiegle/own.html
[KSW04b] M. Kuntz, M. Siegle and E. Werner. CASPA: A Tool for Symbolic Performance and Dependability Evaluation. In Supplemental Volume of Proc. of Int. Conf. on Dependable Systems and Networks (DSN'04), pages 90-91. 2004. http://fakinf.informatik.unibw-muenchen.de/~msiegle/own.html
[BCM+04] R. Barbuti, S. Cataudella, A. Maggiolo-Schettini, P. Milazzo and A. Troina. A Probabilistic Calculus for Molecular Systems. In Proc. Concurrency Specification and Programming (CS&P'04). 2004. [bib] http://www.di.unipi.it/~milazzo/
[Gol04] M. Goldsmith. CSP: The Best Concurrent-System Description Language in the World - Probably!. In Proc. Communicating Process Architectures (CPA'04). 2004. [bib] http://www.wotug.org/cpa2004/programme.shtml
[HLM04] R. Heckel, G. Lajios and S. Menge. Stochastic Graph Transformation Systems. In Proc. 2nd International Conference on Graph Transformations (ICGT'04), volume 3256 of LNCS, pages 210-225, Springer. October 2004. [bib] http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3256&spage=210
[GHHK04] S. Gilmore, V. Haenel, J. Hillston and L. Kloul. PEPA nets in practice: Modelling a decentralised peer-to-peer emergency medical application. In Proc. 1st European Performance Evaluation Workshop (EPEW'04), volume 3236 of LNCS, pages 262-277, Springer-Verlag. October 2004. http://www.dcs.ed.ac.uk/home/stg/
[FP04] W. Fokkink and J. Pang. Simplifying Itai-Rodeh leader election for anonymous rings. In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 53-68, Elsevier Science. September 2004. [bib] http://www.lix.polytechnique.fr/~pangjun/research/pub.html
[DSS04] R. Dingledine, V. Shmatikov and P. Syverson. Synchronous Batching: From Cascades to Free Routes. In Proc. 4th Workshop on Privacy Enhancing Technologies (PET). May 2004. [bib] http://www.csl.sri.com/users/shmat/
[BS04] D. Bhaduri and S. Shukla. NANOPRISM: A Tool for Evaluating Granularity vs. Reliability Trade-offs in Nano Architectures. In Proc. 14th Great Lakes Symposium on VLSI (GLSVLSI'04), ACM. April 2004. http://fermat.ece.vt.edu/Fermatian_Info/debayan.html#Recent Publications
[LMST04] R. Lanotte, A. Maggiolo-Schettini and A. Troina. Automatic Analysis of a Non-Repudiation Protocol. In Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04). March 2004. [bib] http://www.di.unipi.it/~troina/
[DDS04] D. D'Aprile, S. Donatelli and J. Sproston. CSL Model Checking for the GreatSPN Tool. In C. Aykanat, T. Dayar and I. Korpeoglu (editors), International Symposium on Computer and Information Sciences, volume 3280 of Lecture Notes in Computer Science, pages 543-552, Springer Verlag. 2004. http://www.di.unito.it/~sproston/Research/research.html

2003

[GK03] S. Gilmore and L. Kloul. A unified tool for performance modelling and predicition. In Proc. 22nd International Conference on Computer Safety, Reliability and Security (SAFECOMP'03), volume 2788 of LNCS, pages 179-192, Springer-Verlag. September 2003. http://www.dcs.ed.ac.uk/home/stg/
[JPS03] J. Jayaputera, I. Poernomo, H. Schmidt. Timed Probabilistic Reasoning on UML Specialization for Fault Tolerant Component Based Architectures. In Proc. Specification and Verification of Component-Based Systems (SAVCBS'03), Workshop at ESEC/FSE'03. September 2003. http://www.cs.iastate.edu/~leavens/SAVCBS/2003/papers/index.shtml
[GHKR03] S. Gilmore, J. Hillston, L. Kloul and M. Ribaudo. Performance modelling with PEPA nets and PRISM. In Proc. 2nd Workshop on Process Algebra and Stochastically Timed Activities (PASTA Secondi Piatti), pages 23-39. June 2003. http://www.dcs.ed.ac.uk/home/stg/

2002

[JHK02] D. Jansen, H. Hermanns and J.-P. Katoen. A Probabilistic Extension of UML Statecharts Specification and Verification. In Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 355-374, Springer-Verlag. September 2002. http://depend.cs.uni-sb.de/?id=200
[Shm02] V. Shmatikov. Probabilistic Analysis of Anonymity. In Proc. 15th IEEE Computer Security Foundations Workshop (CSFW'02), pages 119-128, IEEE CS Press. June 2002. [bib] http://www.cs.utexas.edu/~shmat/index.html

Theses

2018

[Sal18] Maria Salama. Architectural Stability Of Self-Adaptive Software Systems. Ph.D. thesis, University of Birmingham. 2018. [Studies architectural stability of self-adaptive software systems, including trade-off analysis using PRISM-games.]

2015

[Fra15] Joao Miguel Costa Sousa Franco. Automated Reliability Prediction and Analysis from Software Architectures. Ph.D. thesis, University of Coimbra. 2015. [Proposes automated techniques for predicting the reliability of software architectures, including the use of PRISM for model analysis.]

2012

[Kum12] Jayanand Asok Kumar. Statistical Guarantees of Performance for RTL Designs. Ph.D. thesis, University of Illinois at Urbana-Champaign. 2012. [bib]

2011

[Bak11] Rena Bakhshi. Gossiping Models: Formal Analysis of Epidemic Protocols. Ph.D. thesis, Vrije Universiteit, Amsterdam. 2011. [bib] http://dare.ubvu.vu.nl/handle/1871/18387

2010

[And10] E. André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, L'École Normale Supérieure de Cachan. 2010. [bib] http://www.lsv.ens-cachan.fr/~andre/
[Jar10] Yosr Jarraya. Verification and Validation of UML and SysML Based Systems Engineering Design Models. Ph.D. thesis, Concordia University. 2010. [bib]

2009

[Wer09] Frank Werner. Applied Formal Methods in Wireless Sensor Networks. Ph.D. thesis, University of Karlsruhe. 2009.

Technical reports

2011

[Dut11] Bruno Dutertre. Probabilistic Analysis of Distributed Fault-Tolerant Systems. Technical report CR–2011-217090, NASA. 2011. http://ntrs.nasa.gov/search.jsp?R=20110011564

2007

[HVH07] Tran Thi Bich Hanh and Dang Van Hung. Verification of an Air-Traffic Control System with Probabilistic Real-time Model-checking. Technical report , UNU-IIST United Nations University International Institute for Software Technology. 2007. [bib]

2005

[GW05] M. Goldsmith and P. Whittaker. A CSP Frontend for Probabilistic Tools. Technical report FORWARD Deliverable D14, Formal Systems (Europe Ltd). June 2005. [bib] http://www.forward-project.org.uk/PDF_Files/D14.pdf
[BML05a] M. ter Beek, M. Massink, and D. Latella. Towards Model Checking Stochastic Aspects of the thinkteam User Interface - FULL VERSION. Technical report 2005-TR-18, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche. 2005. [bib] http://fmt.isti.cnr.it/WEBPAPER/TRdsvis.pdf

Other

2005

[GNP05] S. Gay, R. Nagarajan and N. Papanikolaou. Probabilistic Model Checking of Quantum Protocols. Quantum Physics Repository article quant-ph/0504007. April 2005. http://arxiv.org/abs/quant-ph/0504007

Sort by: date, type, title, subject

PRISM Bibliography (external)

Book chapters

2009

Journal papers

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

Conference papers

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Theses

2018

2015

2012

2011

2010

2009

2008

2007

2006

2004

2003

Technical reports

2011

2007

2005

Other

2005

Publications