www.prismmodelchecker.org

PRISM News

November 2023: PRISM-games 3.2 is now available, including symbolic model checking of turn-based stochastic games, correlated/fair equilibria and more. Further information here.
October 2023: A postdoc position is available now at Oxford on the FAIR project. Applications close on 28th November 2023. See here for more details.
October 2023: Two postdoc positions are available now on the FUN2MODEL project. Applications close on 6th November 2023. See here for more details.
September 2023: Dave Parker is giving a keynote talk at QEST / CONFEST 2023 on "Multi-Agent Verification and Control with Probabilistic Model Checking". There is an accompanying paper here.
July 2023: PRISM 4.8 is now available, including uncertain models (IMDPs, IDTMCs) and improved strategy generation. More information here.
May 2022: New survey paper covering MDPs, POMDPs, stochastic games and their support in PRISM and PRISM-games and their support in PRISM and PRISM-games now available.
February 2022: Distinguished paper award at AAAI-22 for this paper, which builds on new interval MDP model checking in PRISM.
January 2022: We are looking for 2 motivated Research Associates to play key roles on the FUN2MODEL project. Applications close on 7th February. See here for more details.
September 2021: PRISM is 20 years old this month! It's first official release was in 2001. Thanks to all those have used it and who have helped develop it over the years.
March 2021: PRISM 4.7 is now available, including support for POMDPs, improved accuracy reporting and more.
February 2021: We are looking for a senior researcher to play a key role on the FUN2MODEL project. Applications close on 12th March, with interviews expected to be held from 29th March 2020 onwards. See here for more details.
January 2021: There are now over 400 papers by external research teams using or building on PRISM. Thanks for your support!
November 2020: Dave Parker is giving a keynote at iFM 2020 on "Verification with Stochastic Games: Advances and Challenges".
September 2020: Marta Kwiatkowska is giving a keynote at KR 2020 on "Probabilistic model checking for strategic equilibria-based decision making".
May 2020: PRISM-games 3.0 is now available, providing concurrent stochastic games, equilibria, real-time models and many new examples.
April 2020: PRISM 4.6 is now available, including a wide range of updates and fixes for users and developers. More information here.
March 2020: We are looking for a research associate to work on probabilistic reasoning for multi-agent systems on the FUN2MODEL project. Applications close on 15th April, with interviews expect in the week of 20th April 2020. See here for more details.
February 2020: We are looking for a senior researcher to play a key role on the FUN2MODEL project. Applications close on 4th March, with interviews to be held on 11th March 2020. See here for more details.
January 2020: PRISM-games 3.0 is now available as a beta release, providing concurrent stochastic games, equilibria, real-time models and many new examples.
September 2019: Senior researcher position and studentship are available at Oxford on the forthcoming FUN2MODEL project project. Applications close 30th October and 28th October respectively, and interviews will be on 8th November 2019. See here and here for more details.
June 2019: Three postdoctoral positions are now available at Oxford on the forthcoming FUN2MODEL project. Applications close 8 July 2019. See here, here and here for more details.
June 2019: Two fully funded ERC Doctoral Studentships are now available at Oxford on the forthcoming FUN2MODEL project. Applications close 8 July 2019. See here for more details.
May 2019: PRISM-games 2.1 is now available, providing simpler installation/compilation, updates from PRISM 4.5 and more. More information here.
April 2019: PRISM 4.5 is now available, including a wide range of updates and fixes for users and developers. More information here.
March 2019: Marta Kwiatkowska has been awarded an ERC Advanced Grant titled "FUN2MODEL: From FUNction-based TO MOdel-based automated probabilistic reasoning for DEep Learning"", which aims to make advances towards provably robust 'strong' Artificial Intelligence. More details here.
January 2019: PRISM just competed in QComp 2019: the inaugural "Comparison of Tools for the Analysis of Quantitative Formal Models"". See the report to appear at TACAS'19 as part of Toolympics.
August 2018: The paper "Using Probabilistic Model Checking for Dynamic Power Management" is one of 5 selected to "highlight important developments for the scientific community" as part of the 30-year anniversary of the journal Formal Aspects of Computing.
August 2018: Dave Parker is giving an invited talk at the 2018 Highlights of Logic, Games and Automata conference on "Probabilistic Model Checking: Advances and Applications", summarising recent developments and future directions for PRISM.
July 2017: PRISM 4.4 is now available, including interval iteration, topological iteration, new reward operators, CTL/LTL model checking and much more.
September 2016: A 2-3 year postdoc position is available now at Birmingham, working with Dave Parker on verification of probabilistic programming languages. Details here.
July 2016: Marta Kwiatkowska, Gethin Norman and Dave Parker have been given the 2016 HVC award for "the invention, development and maintenance of the PRISM probabilistic model checker". For more details, see here.
July 2016: A 3-year postdoc and a PhD position are available now at Birmingham, working with Dave Parker on a new project under the DARPA-funded BRASS program. This will be advertised shortly. Please contact him directly for details.
February 2016: We are delighted to announce that PRISM has again been selected to participate in Google Summer of Code. Contribute to PRISM and get paid for it! More details here and a news item here.
November 2015: We are pleased to report that PRISM has now been downloaded more than 50,000 times. Thanks for your support!
October 2015: Version 2.0 of PRISM-games is out, featuring new reward properties, multi-objective strategy synthesis and assume-guarantee reasoning. More info here.
September 2015: Dave Parker will give a lecture on "Probabilistic Model Checking and Controller Synthesis" at the 2nd AVACS Autumn School on 1 October. See here for resources.
July 2015: A beta release of PRISM version 4.3 is now available. New features include external LTL-to-automata converters and various new model checking algorithms. Details here.
June 2015: PRISM now supports the HOA (Hanoi Omega Automata) format. This allows external LTL-to-automaton converters to be used. More details in this CAV'15 paper.
February 2015: Three postdoctoral positions available to work on the 5-year Programme Grant "Mobile Robotics: Enabling a Pervasive Technology of the Future", held by Paul Newman and Ingmar Posner (Oxford's Engineering Science) and Niki Trigoni and Marta Kwiatkowska (Oxford's Computer Science). More details here.
November 2014: Marta Kwiatkowska has been awarded an honorary doctorate from KTH Royal Institute of Technology. More details here.
August 2014: Here is a new report, published by the LMS and the Smith Institute, giving an accessible introduction to quantitative verification.
July 2014: Two PRISM-related postdoctoral positions are now available at Birmingham on the HIERATIC project. See the advert. The posts run until 30 Sep 2015. Applications close 17 Aug 2014.
July 2014: Dave Parker will give a session on "Probabilistic real-time systems" at the MOVEP'14 summer-school on 7 July. See here for resources.
May 2014: Marta Kwiatkowska will give a course on "Probabilistic model checking with PRISM" at the SSFT'14 summer-school this month. See this page for resources.
May 2014: A beta release of PRISM version 4.2 is now available. New features include featuring parametric model checking, fast adaptive uniformisation and more.
April 2014: We are delighted that PRISM has again been selected for the Google Summer of Code programme. This year we will have 8 students joining us.
February 2014: We are delighted to announce that PRISM has again been selected to participate in Google Summer of Code. Contribute to PRISM and get paid for it! More details here and a news item here.
November 2013: A new development version of PRISM is now available, featuring parametric model checking, fast adaptive uniformisation and more.
September 2013: See the upcoming tutorial and keynote at ATVA'13 by Marta Kwiatkowska on probabilistic model checking, strategy synthesis and PRISM.
August 2013: Two more postdoctoral positions are available in automated verification and synthesis on the ERC Advanced Investigator Grant VERIWARE. Candidates with prior experience of applications to biology are particularly encouraged to apply. Applications close 30 Sep 2013. See here for more details.
May 2013: A postdoc position is now available at Birmingham on the new project "Automated Game-Theoretic Verification of Security Systems". Details here. Applications close on 4 Sep 2013.
Jun 2013: A fully funded PhD studentship is now available at Birmingham on the topic "Quantitative Verification of Complex Systems". See here for more details.
Jun 2013: Congratulations to Alessandro Bruni and Proteek Roy, who have been selected to work on PRISM as part of GSoC 2013, and also to Jan Gorzny, who will work on PRISM as part of a JPF GSoC project.
May 2013: Two postdoctoral positions are now available in automated verification and synthesis on the ERC Advanced Investigator Grant VERIWARE. Applications close on 31st May 2013. See here for more details.
April 2013: We are delighted to announce that PRISM has been selected to participate in the 2013 Google Summer of Code. Contribute to PRISM and get paid for it! More details here and here.
April 2013: PRISM features this week in a tutorial on probabilistic hybrid systems at CPSWeek 2013, run by Marta Kwiatkowska and Holger Hermanns.
March 2013: PRISM-games an extension of PRISM for probabilistic model checking of stochastic multi-player games will be presented at TACAS'13 this week. Read the tool paper or visit the website for more information.
October 2012: A postdoctoral position is now available at Birmingham on the new HIERATIC project. See the advert, the particulars and apply here. Applications close 22 Oct 2012.
September 2012: Interested in probabilistic model checking for probabilistic timed automata? A new tutorial paper is now available, to appear in Formal Methods in System Design.
September 2012: Nature Scientific Reports publish a paper by Luca Cardelli & Attila Csikász-Nagy that uses PRISM to study cell cycle switch as a computing device. See here for details.
September 2012: Marta Kwiatkowska will give this year's Milner Lecture, entitled "Sensing everywhere: on quantitative verification for ubiquitous computing", at the University of Edinburgh on 25 Sep 2012.
July 2012: A postdoctoral position is now available at Birmingham on the forthcoming HIERATIC project. See the advert, the particulars and apply here. Applications close 14 Aug 2012.
April 2012: Two postdoctoral positions are now available at Oxford on the VERIWARE and Autonomous Ubiquitous Sensing projects. Applications close 25 April 2012. See here and here for more details.
February 2012: We are pleased to announce the release of PRISM-games, a new extension of PRISM for model checking stochastic multi-player games.
February 2012: PRISM has now been downloaded more than 25,000 times. Thanks for your support.
August 2010: Marta Kwiatkowska will give a course on "Advances in Probabilistic Model Checking" at the Marktoberdorf 2011 summer-school this month. See this page for resources.
July 2011: To coincide with the recent release of PRISM 4.0, we are pleased to announce the new PRISM benchmark suite, for testing or evaluating probabilistic model checking tools and techniques.
July 2011: Congratulations to Shinji Kikuchi and Yasuhide Matsumoto from Fujitsu, who won the Best Paper award for their new paper applying PRISM to cloud computing systems.
May 2011: The final beta release of PRISM 4.0, which includes support for probabilistic timed automata (PTAs) and statistical model checking, is available on the main download page.
March 2011: Interested in probabilistic model checking for MDPs? A new tutorial paper on the subject, written for the SFM-11:CONNECT summer-school, is now available.
February 2011: A fully funded PhD studentship is now available at Oxford on the topic "Automated Verification Techniques for DNA Computing". Applications close 28 Feb 2011. See here for more details.
December 2010: An early release of PRISM 4.0 is now available as a development version. This includes support for probabilistic timed automata (PTAs) and statistical model checking.
November 2010: A 1-year postdoc position is now available at Oxford on the PRISMATIC project. Applications close 8 Dec 2010. See here for more details.
October 2010: A fully funded PhD studentship is now available at Oxford on the new VERIWARE project. Applications close 15 Nov 2010. See here for more details.
September 2010: US R&D company SIFT is hiring researchers in probabilistic verification. See here for details.
August 2010: The paper "Probabilistic Model Checking of Complex Biological Pathways", by John Heath, Marta Kwiatkowska, Gethin Norman, David Parker and Oksana Tymchyshyn, was recently awarded the Top Cited Article award in the journal Theoretical Computer Science, for the period 2005-2010.
July 2010: Marta Kwiatkowska and Dave Parker will give a 5-part course on "Probabilistic Model Checking" at the ESSLLI'10 summer-school in Copenhagen next month.
June 2010: Interested in applying PRISM to systems biology? This new book chapter in "Symbolic Systems Biology: Theory and Methods" provides a tutorial and exercises on the subject.
April 2010: A 2-year postdoc position is now available at Oxford on the Predictable Software Systems project. Applications close 28 May 2010. See here for more details.
March 2010: Two postdoctoral positions are now available at Oxford on the forthcoming VERIWARE project. Applications close 7 May 2010. See here for more details.
March 2010: Two fully funded PhD studentships are now available at Oxford on the forthcoming VERIWARE project. Applications close 4 May 2010. See here for more details.
February 2010: There will be a PRISM session at this month's PhD school on Quantitative Model Checking (QMC), organised by ArtistDesign/MT-LAB.
May 2009: A beta release of PRISM version 3.3 is now available. New features include LTL model checking, better error reporting, an extended property language and much more.
December 2008: A new development version of PRISM is now available, with many new features and improvements. Full details here.
November 2008: Two research positions are now available at Oxford, working on the CONNECT-IP project: one Research Assistant (Grade 7) and one Student Researcher. Applications close 5 January 2009. See here and here for more details.
April 2008: A fully funded PhD studentship is now available at Oxford on the forthcoming Predictable Software Systems project. Applications close 16 May 208. See here for more details.
March 2008: PRISM has now been downloaded more than 10,000 times. Thanks for your support.
February 2008: A beta version of the next PRISM release (version 3.2) is now available. See here for details.
November 2007: A fully funded PhD studentship is now available at Oxford on the forthcoming Predictable Software Systems project. Applications close 18 January. See here for more details.
October 2007: A new development version of PRISM is now available. Changes since the last development release include a new graph plotting engine, improvements to labels/formula, and a (slight) redesign to match the new web site.
September 2007: A postdoctoral position is now available at Oxford on the forthcoming Predictable Software Systems project. Applications close 18 October. See here for more details.
July 2007: The PRISM team have moved to Oxford University. Concurrently, we have re-launched the PRISM web site, with a new design and a new URL.
June 2007: New development versions of PRISM are now being made available again. Recent new functionality includes: an SBML-to-PRISM translator, support for 64-bit architectures and an improved simulator GUI.
May 2007: A new FAQ section has been added to the PRISM manual. Comments or requests for topics to be covered are welcome.
May 2007: A new symmetry reduction tool for PRISM called GRIP, developed at the University of Glasgow, is now available.
April 2007: The PRISM web site now includes slides for an 11-part lecture course introducing probabilistic model checking and PRISM. This material formed the basis of the recent 15-hour course given at the BISS 2007 school.
April 2007: Version 3.1.1 of PRISM has now been released, including a few small but important bug fixes (precise details here).
November 2006: A beta release of version 3.1 of PRISM is now available. New features include a Windows installer, multiple reward structures and command-line generation of random paths (more details here).
October 2006: New and up-to-date material for those wishing to learn about PRISM is now available, to coincide with the VPSM PhD school in Copenhagen this month. An online tutorial is now available. There are also up-to-date slides. These are in three parts: (I) probabilistic model checking for DTMCs/MDPs/PTAs, (II) PRISM and (III) case studies.
July 2006: The PRISM manual is now online, making it considerably easier to navigate and search. This will also allow us to update and improve the manual more efficiently. This launch coincides with the full release of version 3.0 of PRISM, which was previously available as a beta release.
June 2006: Applications are invited for a Research Associate to work on the new EPSRC funded project Automated quantitative software verification with PRISM, whose aim is to extend the PRISM tool with the capability to extract models from software. Details of the post can be found here. Informal enquires can be emailed to Marta Kwiatkowska.
March 2006: Version 3.0.beta1 of PRISM is now available. This major new release includes a simulator (providing approximate verification techniques and a model debugging tool), costs and rewards, support for Mac OS X, improved import/export functionality and much more.
March 2006: A tool paper [HKNP06] and demo of the forthcoming new release of PRISM will be presented at the TACAS'06 conference in Vienna this month.
March 2006: There will be a tutorial on probabilistic model checking and PRISM at the Verification of Protocols for Security and Mobility (VPSM) PhD School to be held in Copenhagen in October.
January 2006: We are in the process of migrating "support" aspects of the PRISM project to SourceForge. The project page is here. Please help out by posting queries in the help forum or filing a bug report.
October 2005: PRISM now runs on Mac OS X, as well as on Linux, Solaris and Windows. To try it out, download a development version of PRISM.
June 2005: A PhD studentship is now available in the School of Computer Science at the University of Birmingham to work on probabilistic model checking and PRISM. See here and here for more information.
January 2005: Recent development versions of PRISM are now being made available from here. These versions add various new features, including support for analysis of models which include information about costs and rewards.
September 2004: PRISM now runs on Windows, as well as on Linux and Solaris. This new functionality is available in version 2.1, the current release of PRISM, which can be downloaded from here.
April 2004: The book Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems has now been published by AMS. This includes six chapters of lecture notes covering the background of probabilistic model checking and the PRISM tool. See here for more information.
March 2004: Version 2.0 of PRISM is now available. The new release includes significant improvements to the PRISM modelling language and a completely new graphical user interface. See here for more precise details of what is included. To download PRISM 2.0, click here.

About PRISM