Propositional Dynamic Logic (PDL) [1] is a logic in which abstract properties about the behaviour of programs can be expressed, in a very general way. Because of its generality it is suitable for checking the behaviour or a wide range of programs and systems, via model checking. PDL is what is known as a modal … full description “A Cyclic Prover for Propositional Dynamic Logic (available)”
Supervisor: Reuben Rowe
Active: updated 3-FEB-2026 (OSAA035) no expiry
Building a Benchmark Suite for Modal Mu-Calculus (available)
The modal mu-calculus [1] is a logic for expressing properties of abstract state transition systems, and generalises other logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Because of this, it is a very useful tool for describing and verifying the behaviour of computer systems. The aim of this project is to support … full description “Building a Benchmark Suite for Modal Mu-Calculus (available)”
Cyclist: Verifying Programs using Cyclic Proof (available)
Cyclic proofs are a technique for proving properties inductively, or proving properties about inductively defined objects or processes. They can be used to prove logical statements, or to verify recursive programs. The Cyclist tool [1] has been developed as an automatic verification tool based on cyclic proofs. It can prove termination and verify temporal properties … full description “Cyclist: Verifying Programs using Cyclic Proof (available)”
Deciding Isomorphism for Infinite Descent Problems (available)
The Infinite Descent property underpins two very important applications in program verification: termination of programs [1,2], on the one hand, and correctness of cyclic proofs of formulas or properties [3], on the other. In both cases, the object of interest (i.e. a program or a proof) is converted into an abstract form for which the … full description “Deciding Isomorphism for Infinite Descent Problems (available)”
Formalising Recursive Adaptive Grammars using a Proof Assistant (available)
The aim of this project is to formalise using proof assistant (such as Rocq [1], Agda [4], or Isabelle [5]) the meta-theory of the recursive adaptive grammar framework [2] Programming languages are usually specified on two levels. The first level defines a context-free grammar that specifies the syntax of the language. Usually, however, not all … full description “Formalising Recursive Adaptive Grammars using a Proof Assistant (available)”