News

Monday 6th January 2025

Isabelle2024 Release

We have just published versions of Isabelle/UTP that are built against Isabelle2024, which can be found on the Download page.

Monday 30th September 2024

Paper accepted on Interaction Trees accepted

We recently had a paper accepted for publication in ACM Transactions on Software Engineering and Methodology entitled "Unifying Model Execution and Deduction Verification with Interaction Trees in Isabelle/HOL". This paper integrates ITrees into Isabelle/UTP to support both execution and verification of models, including imperative programs, Circus processes, and Z-Machines. A first look version can be found here: https://dl.acm.org/doi/10.1145/3702981.

Thursday 20th April 2023

Paper accepted on Z-Machines

Fang Yan has recently has a paper accepted at ICECCS 2023 entitled "Automated Compositional Verification for Robotic State Machines using Isabelle/HOL", which applies the Z-Machine notation in Isabelle/UTP, for verification of RoboChart state machines.

Monday 6th March 2023

Isabelle2022 Release with Hybrid Verification

We have made a new release of the Isabelle/UTP archive, which uses Isabelle 2022. The new archive also includes a session called Hybrid-Verification, which contains our verification tool for hybrid dynamical systems, as documented in our FM2021 paper. Various other updates have been made to the other components, in line with the GitHub histories.

Wednesday 4th January 2023

New website

We are pleased to present our new website for Isabelle/UTP, which has much more content than the old one, and we hope to keep more up-to-date.