News & Activities [show all]

• December 2021: Congratulations to Edoardo Bacci, who successfully defended his PhD thesis "Formal Verification of Deep Reinforcement Learning Agents" this week (see papers in FORMATS'20 and IJCAI'21).
• November 2021: New survey paper Probabilistic Model Checking and Autonomy to appear in Annual Review of Control, Robotics, and Autonomous Systems next year, covering MDPs, POMDPs and stochastic games.
• November 2021: I'll be PC co-chair of FORMATS 2022 with Sergiy Bogomolov, to be held in Warsaw in September 2022. Submit your papers!
• 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.
• September 2021: I'm happy to announce that I'll be a Turing Fellow at the Alan Turing Institute from October 2021, working on formal verification of AI systems.
• August 2021: Congratulations to Fatma Faruq, who successfully defended her PhD thesis "Verified Multi-Robot Planning Under Uncertainty" this week.
• July 2021: I am giving an invited tutorial at EXPRESS/SOS 2021 next month on "Probabilistic Verification of Concurrent Autonomous Systems".
• May 2021: New paper on time-unbounded verification of reinforcement learning to appear at IJCAI 2021.
• May 2021: Congratulations to Michael Oxford, who successfully defended his PhD thesis "Quantitative Verification of Gossip Protocols for Certificate Transparency" this week.
• Mar 2021: PRISM 4.7 is now available, including support for POMDPs, improved accuracy reporting and more.
• Jan 2021: There are now over 400 papers by external research teams using or building on PRISM.
• Jan 2021: Congratulations to Irfan Muhammad, who successfully defended his PhD thesis "Algorithms for Reachability Problems on Stochastic Markov Reward Models" this week.
• Dec 2020: New paper to appear in Formal Methods in System Design covering our recent thread of work on on verifying concurrent stochastic games, as implemented in PRISM-games.
• Nov 2020: I'll be giving a keynote at iFM 2020, (International Conference on integrated Formal Methods) on "Verification with Stochastic Games: Advances and Challenges".
• Jul 2020: New paper on probabilistic guarantees for deep reinforcement learning to appear at FORMATS 2020.
• Jul 2020: New paper on verifying multi-coalition equilibria for concurrent stochastic games to appear at QEST 2020.
• May 2020: New paper at CAV 2020 describing version 3.0 of PRISM-games, featuring concurrent stochastic games, equilibria, real-time models and many new examples.
• May 2020: Congratulations to Alexandros Evangelidis, who successfully defended his PhD thesis "Verified Control and Estimation for Cloud Computing" this week (see papers in CCGrid'17, FGCS and FM'19).
• Apr 2019: The papers for TACAS 2020 are now online. Sadly, ETAPS could not happen as planned in April, but the papers are all open access and available.
• Jan 2020: PRISM-games version 3.0 is now available, providing concurrent stochastic games, equilibria, real-time models and many new examples. More information here.
• Oct 2019: Attending Dagstuhl seminar "Analysis of Autonomous Mobile Collectives in Complex Physical Environments".
• Sep 2019: Welcome to new PhD student Dan Fentham, working on the NCSC/GCHQ-sponsored "Adversarially-robust neural networks for cyber security" project.
• Jul 2019: New paper to appear at ESORICS 2019 on automated detection of side channels in probabilistic systems, including the SCH-IMP tool, which builds upon PRISM-pomdps.
• July 2019: We have finalised the programme for QEST 2019. There are some great invited talks, tutorials and papers. Please attend! Details http://www.qest.org/qest2019/program.html.
• July 2019: New paper to appear at FM 2019 on verifying stochastic games using Nash equilibria.
• July 2019: New paper to appear at FM 2019 on verifying numerical stability properties of Kalman filters.
• June 2019: I'm giving an invited talk on "Multi-objective Reasoning with Probabilistic Model Checking" at MoRe 2019 (Multi-objective Reasoning in Verification and Synthesis) in Vancouver.
• June 2019: I'll be PC co-chair of TACAS 2020 with Armin Biere, to be held in Dublin in April 2020. Submit your papers!
• May 2019: PRISM-games version 2.1 is now available, providing simpler installation/compilation, updates from PRISM 4.5 and more. More information here.
• May 2019: New paper to appear in IJRR (International Journal of Robotics Research) on "Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots", with Fatma Faruq, Nick Hawes and Bruno Lacerda.
• Apr 2019: PRISM 4.5 is now available, including a wide range of updates and fixes for users and developers. More information here.
• Mar 2019: Mark Ryan and I have a fully-funded PhD position on "adversarially-robust neural networks for cyber security" sponsored by GCHQ and the National Cyber Security Centre (NCSC). See here for details and to apply.
• Feb 2019: New paper in Nature Scientific Reports describing work on a mitotic spindle assembly checkpoint case study using techniques developed on the HIERATIC project.
• Jan 2019: The Quantitative Verification Benchmark Set is a new set of benchmarks for probabilistic model checking across a range of probabilistic models, complementing the existing PRISM Benchmark Suite . See our TACAS'19 paper for details.
• Jan 2019: New paper "Software Adaptation for an Unmanned Undersea Vehicle" in IEEE Software giving a high level overview of work on the DARPA-funded PRINCESS project.
• Jan 2019: PRISM just competed in QComp 2019: the inaugural Comparison of Tools for the Analysis of Quantitative Formal Models. See our report to appear at TACAS'19 as part of Toolympics.
• Sep 2018: I'll be co-chairing QEST 2019 (Intl. Conference on Quantitative Evaluation of SysTems), to held in Glasgow next September, with Verena Wolf and Gethin Norman. Please submit your papers!
• Sep 2018: At the 2018 Highlights of Logic, Games and Automata conference in Berlin, giving an invited talk on "Probabilistic Model Checking: Advances and Applications"
• Aug 2018: Our 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.
• Aug 2017: New paper to appear at IROS 2018 on multi-robot task allocation and planning under uncertainty, with Fatma Faruq, Nick Hawes and Bruno Lacerda.
• May 2018: Two new PRISM-games papers: (i) one on an extension for concurrent stochastic games, to appear at QEST 2018; (ii) an extended tool paper in STTT summarising the tool and its applications.
• Apr 2018: Congratulations to Nishan Kamaleson, who successfully completed his PhD on "Model Reduction Techniques for Probabilistic Verification of Markov Chains".
• Sep 2017: Welcome to new PhD students Edoardo Bacci and James Kelly
• Jul 2017: Version 4.4 of PRISM is out now, including interval iteration (see this CAV'17 paper), topological iteration, new reward operators, CTL/LTL model checking and much more.
• Jun 2017: Congratulations to Ahmed Al-Ajeli, who successfully defended his PhD thesis "Fourier-Motzkin Methods for Fault Diagnosis in Discrete Event Systems" this week.
• Jun 2017: New paper to appear at CAV 2017 on building a more reliable probabilistic model checker with interval iteration.
• May 2017: New book chapter on advances and applications in probabilistic model checking, to appear in the forthcoming Formal System Verification
• April 2017: New paper to appear at ICAPS 2017 on probabilistic time-bounded guarantees for mobile robots.
• Mar 2017: Welcome to new postdoc Chris Novakavic, working on the DARPA-funded PRINCESS project.
• Feb 2017: Welcome to new PhD student Fatma Faruq.
• Feb 2017: New paper to appear at CCGrid 2017 on verification of cloud-based auto-scaling policies.
• Jan 2017: A 2-3 year postdoc position is available to work with me at Birmingham on formal verification for probabilistic systems, under the DARPA-funded BRASS program. Details here. Contact me for details.
• Nov 2016: At HVC 2016 in Haifa, for the HVC award. Presentation: "Probabilistic Model Checking: Past, Present & Future".
• Sep 2016: Welcome to new PhD students Michael Oxford and Irfan Muhammad.
• Aug 2016: I'm Tools Chair for TACAS 2017. Submit your tool papers now!
• Jul 2016: I've been awarded, jointly with Marta Kwiatkowska and Gethin Norman, the 2016 HVC award for "the invention, development and maintenance of the PRISM probabilistic model checker". For more details, see here.
• Jul 2016: I'm hiring a postdoc and a PhD student to work on a new project under the DARPA-funded BRASS program. This will be advertised shortly. Please contact me directly for details.
• Jun 2016: I'm giving a tutorial with Nick Hawes at the ICAPS'16 summer school next week on "Formal Guarantees for Robotic Navigation Planning", in the session "Task Scheduling and Execution for Long-Term Autonomy".
  
• Jun 2016: New paper on verification and strategy synthesis for attack-defence trees, appearing at CSF'16 this month.
• Feb 2016: PRISM has been selected to participate in Google Summer of Code 2016.
  Contribute to PRISM and get paid for it! See here for details if you're interested.
• Feb 2016: New paper on finite-horizon probabilistic bisimulation to appear at SPIN'16.
• Dec 2015: Version 2.0 of PRISM-games is out, featuring multi-objective and compositional strategy synthesis. See our TACAS'16 paper for details.
• Nov 2015: Seminar at the University of Southampton: "Probabilistic Model Checking and Strategy Synthesis".
• Oct 2015: Lecture at the AVACS Autumn School in Oldenburg: "Probabilistic Model Checking and Controller Synthesis".
• Sep 2015: I'll be contributing to the panel "Agent Verification: Current Research Challenges" at the the Agent Verification Workshop in Liverpool this week.
• Jul 2015: PRISM now officially supports the new Hanoi Omega-Automata format. See our CAV'15 paper for details.
• Jun 2015: New paper on partially observable probabilistic real-time systems, to appear in FORMATS 2015.
• Jun 2015: Congratulations to Mateusz Ujma, who just successfully defended his thesis "On Verification and Controller Synthesis for Probabilistic Systems at Runtime".
• May 2015: Talk at the Autonomous Intelligent Machines and Systems (AIMS) CDT, University of Oxford:
  "Probabilistic Model Checking and Strategy Synthesis for Robot Navigation".
• May 2015: New paper applying multi-objective probabilistic model checking to robot navigation, to appear in IJCAI 2015.
• Apr 2015: Attending Dagstuhl seminar "Challenges and Trends in Probabilistic Programming".
• Apr 2015: New paper on permissive controller synthesis to appear in LMCS (extended version of TACAS'14 paper).
• Oct 2014: Talk at the University of California, Berkeley in the DREAMS seminar series (Design of Robotics and Embedded systems, Analysis, and Modeling Seminars): "Probabilistic Model Checking and Strategy Synthesis".
• Oct 2014: Attending the 2014 Google Summer of Code Reunion event, Mountain View, California.
• Sep 2014: I'm giving a keynote talk at FMICS'14 in Florence this week: "Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance". Slides here.
• Aug 2014: New paper to appear at ATVA'14 on new techniques for verifying Markov decision processes with learning- and heuristic-based approaches.
• Aug 2014: Here is a report I co-wrote, published by the London Mathematical Society and the Smith Institute, giving an accessible introduction to quantitative verification.
• Jul 2014: Two 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.
• Jul 2014: Lecture at the MOVEP'14 (Modelling and Verification of Parallel Processes) summer school in Nantes: "Automated Verification of Probabilistic Real-time Systems". More resources here.
• Jun 2014: New paper to appear at IROS'14 on probabilistic model checking and strategy synthesis for co-safe LTL specifications in robotic systems, with Bruno Lacerda and Nick Hawes.
• May 2014: Here is our contribution to the Festschrift for Prakash Panangaden,
  on "Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations".
• Mar 2014: I'll be lecturing on probabilistic model checking at MOVEP'14
  (the 11th Summer School on Modelling and Verification of Parallel Processes) in Nantes, this July.
• Feb 2014: PRISM has been selected to participate in the 2014 Google Summer of Code.
  Contribute to PRISM and get paid for it! See here for details if you're interested.
• Jan 2014: New paper to appear at TACAS'14 on permissive controller synthesis for stochastic games.
• Nov 2013: Welcome to new post-doc Chunyan Mu, working on this project.
• Oct 2013: Talk at NASA Ames, Robust Software Engineering group:
  "Probabilistic Model Checking and Strategy Synthesis"
• Oct 2013: Tech talk at Google, Mountain View, California:
  "Quantitative Verification: Correctness, Reliability and Beyond"
• Oct 2013: Attending the 2013 Google Summer of Code Mentor Summit, Mountain View, California
• Oct 2013: Welcome to new PhD student Nishanthan Kamaleson.
• Sep 2013: New paper on compositional verification techniques for probabilistic systems
  to appear in Information and Computation (extended version of TACAS'10 paper).
• Aug 2013: Tutorial on "Verification of Probabilistic Real-time Systems"
  at the French Summer School on Real-Time Systems (ETR 2013), Toulouse.
• Aug 2013: Postdoctoral position now available at Birmingham on the new project "Automated Game-Theoretic Verification of Security Systems". See the advert and apply here. Applications close 4 Sep 2013.
• Jul 2013: New paper on abstraction refinement for probabilistic timed programs to appear in Theoretical Computer Science.
• Jul 2013: New overview/tutorial paper on strategy synthesis for probabilistic systems at ATVA'13.
• Jun 2013: Fully funded PhD position at Birmingham on "Quantitative Verification of Complex Systems",
  to start from September 2013 onwards. See here for details.
• May 2013: New paper at CSF'13 on "Probabilistic Point-to-Point Information Leakage".
• Apr 2013: PRISM has been selected to participate in the 2013 Google Summer of Code.
  Contribute to PRISM and get paid for it! Details here. Send me a mail if you're interested.
• Feb 2013: New FMSD paper on model checking of stochastic multi-player games (extended version of TACAS'12 paper).
• Feb 2013: New paper to appear at the 2013 Strategic Reasoning workshop on strategic analysis of user-centric networks.
• Jan 2013: New TACAS'13 tool paper on PRISM-games, a model checker for stochastic multi-player games.
• Dec 2012: Seminar at Imperial College London:
  "Automated Game-theoretic Verification for Probabilistic Systems"
• Dec 2012 Kick-off meeting for the new HIERATIC project, Birmingham, 6-7 Dec.
• Nov 2012: Attending Dagstuhl seminar "Games and Decisions for Rigorous Systems Engineering"
• Nov 2012: VMCAI'13 paper on SMT-based bisimulation for Markov models
• Oct 2012: Postdoctoral position now available at Birmingham on the new HIERATIC project.
  See the advert, the particulars and apply here. Applications close 22 Oct 2012.
• Sep 2012: New tutorial paper on probabilistic timed automata (PTAs) in Formal Methods in System Design
• Jul 2012: Organising SPIN'12 at Oxford, 23-24 July
• Jul 2012: ATVA'12 paper on "Pareto Curves for Probabilistic Model Checking"
• Jul 2012: RV'12 paper on incremental/runtime methods for probabilistic model checking
• Jun 2012: Seminar at Birmingham's Centre for Systems Biology (CSB):
  "Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking"
• May 2012: Departmental seminar at the University of Liverpool:
  "Automatic Verification of Competitive Stochastic Systems"
• May 2012: QEST'12 paper on the new PRISM benchmark suite.
• Mar 2012: TACAS'12 paper on model checking of stochastic multi-player games (and new tool PRISM-games)
• Mar 2012: LFCS seminar at the University of Edinburgh
• Dec 2011: Royal Society Interface paper on probabilistic model checking of DNA circuits
• Jul 2011: CAV'11 tool paper on the new version of PRISM

• • 2021
  • TOSME 2021 (Intl. Workshop on Tools for Stochastic Modelling and Evaluation)
  • SETTA 2021 (Intl. Symposium on Dependable Software Engineering)
  • RV 2021 (Intl. Conference on Runtime Verification)
  • QEST 2021 (Intl. Conference on Quantitative Evaluation of SysTems)
  • R2AW 2021 (Robust and Reliable Autonomy in the Wild)
  • SYNT 2021 (Intl. Workshop on Synthesis)
  • EPEW 2021 (European Performance Engineering Workshop)
  • TACAS 2021 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
  • HSCC 2021 (Intl. Conference on Hybrid Systems: Computation and Control)
  • AAAI 2021 (AAAI Conference on Artificial Intelligence)
  • FM 2021 (Intl. Conference on Formal Methods)
• • 2020
  • SETTA 2020 (Intl. Symposium on Dependable Software Engineering)
  • QEST 2020 (Intl. Conference on Quantitative Evaluation of SysTems)
  • IJCAI-PRICAI 2020 (Intl. Joint Conference on Artificial Intelligence & Pacific Rim Intl. Conference on Artificial Intelligence)
  • TACAS 2020 [PC co-chair] (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
  • MARS 2020 (Intl. Workshop on Models for Formal Analysis of Real Systems)
  • InterAVT 2020 (Interactive Workshop on the Industrial Application of Verification and Testing)
  • AAAI 2020 (AAAI Conference on Artificial Intelligence)
• • 2019
  • QEST 2019 [PC co-chair] (Intl. Conference on Quantitative Evaluation of SysTems)
  • IJCAI 2019 (Intl. Joint Conference on Artificial Intelligence)
  • FT4DAS 2019 (Intl. Workshop on Formal Techniques for Dependable Autonomous Systems)
  • TACAS 2019 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
  • InterAVT 2019 (Interactive Workshop on the Industrial Application of Verification and Testing)
• • 2018
  • ICECCS 2018 (Intl. Conference On Engineering Of Complex Computer Systems)
  • FORMATS 2018 (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
  • TACAS 2018 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
  • IJCAI 2018 (Intl. Joint Conference on Artificial Intelligence)
  • VaVaS 2018 (Intl. Workshop on Verification and Validation of Autonomous Systems)
• • 2017
  • InfQ 2017 (Intl. Workshop on Quantitative Methods in Informatics)
  • TACAS 2017 [Tools chair] (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
  • LATA 2017 (Intl. Conference on Language and Automata Theory and Applications)
  • MARS 2017 (Intl. Workshop on Models for Formal Analysis of Real Systems)
• • 2016
  • CAV 2016 (Intl. Conference on Computer Aided Verification)
  • FORMATS 2016 (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
  • VMCAI 2016 (Intl. Conference on Verification, Model Checking, and Abstract Interpretation)
  • PASM 2016 (Intl. Workshop on Practical Applications of Stochastic Modelling)
• • 2015
  • CAV 2015 (Intl. Conference on Computer Aided Verification)
  • TACAS 2015 (Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems)
  • SEFM 2015 (Intl. Conference on Software Engineering and Formal Methods)
  • CTSE 2015 (Intl. Workshop on Control Theory for Software Engineering)
  • VMCAI 2015 (Intl. Conference on Verification, Model Checking, and Abstract Interpretation)
  • QEST 2015 (Intl. Conference on Quantitative Evaluation of SysTems)
  • QAPL 2015 (Intl. Workshop on Quantitative Aspects of Programming Languages)
• • 2014
  • QEST 2014 [Tools chair] (Intl. Conference on Quantitative Evaluation of SysTems)
  • FORMATS 2014 (Intl. Conference on Formal Modeling and Analysis of Timed Systems)
  • SPIN 2014 (Intl. SPIN Symposium on Model Checking of Software)
  • HPCC 2014 (IEEE Intl. Conference on High Performance Computing and Communications)
  • VEMDP 2014 (Intl. Workshop on Verification of Engineered Molecular Devices and Programs)
  • SEFM 2014 (Intl. Conference on Software Engineering and Formal Methods)
  • FMICS 2014 (Intl. Workshop on Formal Methods for Industrial Critical Systems)
  • QAPL 2014 (Intl. Workshop on Quantitative Aspects of Programming Languages)
  • PASM 2014 (Intl. Workshop on Practical Applications of Stochastic Modelling)
  • GRAPHITE 2014 (Intl. Workshop on Graph Inspection and Traversal Engineering)
  • SIMUTools 2014 (Intl. Conference on Simulation Tools and Techniques)
• • 2013
  • CONCUR 2013 (Intl. Conference on Concurrency Theory)
  • TASE 2013 (Intl. Symposium on Theoretical Aspects of Software Engineering)
  • SPIN 2013 (Intl. SPIN Symposium on Model Checking of Software)
  • CBSE 2013 (Intl. ACM SIGSOFT Symposium on Component-Based Software Engineering)
  • FMICS 2013 (Intl. Workshop on Formal Methods for Industrial Critical Systems)
  • HAS 2013 (Intl. Workshop on Hybrid Autonomous Systems)
  • SIMUTools 2013 (Intl. Conference on Simulation Tools and Techniques)
  • GRAPHITE 2013 (Intl. Workshop on Graph Inspection and Traversal Engineering)
  • FAMES 2013 (Intl. Workshop on Formal Approaches to Managing Evolving Systems)
  • QAPL 2013 (Intl. Workshop on Quantitative Aspects of Programming Languages)
  • SAC 2013-COSYS [PC co-chair] (ACM Symposium on Applied Computing: Cooperative Systems)
  • SAC 2013-SVT (ACM Symposium on Applied Computing: Software Verification & Testing)
• • 2012
  • CMSB 2012 (Intl. Conference on Computational Methods in Systems Biology)
  • SPIN 2012 [PC co-chair] (Intl. SPIN Workshop on Model Checking of Software)
  • PASM 2012 (Intl. Workshop on Practical Applications of Stochastic Modelling)
  • FMICS 2012 (Intl. Workshop on Formal Methods for Industrial Critical Systems)
  • SIMUTools 2012 (Intl. Conference on Simulation Tools and Techniques)
  • QAPL 2012 (Intl. Workshop on Quantitative Aspects of Programming Languages)
  • SAC 2012-SVT (ACM Symposium on Applied Computing, Software Verification & Testing)
  • SAC 2012-COSYS [PC co-chair] (ACM Symposium on Applied Computing)
• • 2011
  • QEST 2011
  • SPIN 2011
  • SAC 2011
  • SIMUTools 2011
  • MASCOTS 2011
  • QAPL 2011
  • PASM 2011
• • ...2010
  • SPIN 2010
  • MASCOTS 2010
  • HiBi 2010
  • QAPL 2010
  • FIT 2010
  • SOCA 2009
  • MASCOTS 2009
  • HiBi 2009
  • PASM 2009
  • TiSto 2009
  • ASHEs 2009
  • QEST 2008
  • CMSB 2008