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)”
Category: Software Engineering
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)”
Empirical evaluation of static verifiers for the Go programming language (available)
Go is a language that natively supports many constructs to synchronise concurrent threads. Because of this, developing code that contains subtle concurrency bugs is rather common. To address this problem, several groups of researchers have put forwards tools to find concurrency bugs in Go codebases. The objective of this project is to evaluate how some … full description “Empirical evaluation of static verifiers for the Go programming language (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)”
Implementation of biologically inspired efficient deep learning models (available)
As deep learning models continue to grow in size and complexity to tackle increasingly difficult tasks, the need for efficient and scalable models becomes ever more important. Extremely large language models like GPT-4 require massive computational resources and expensive hardware to train and run. This makes them impractical to deploy at scale in many real-world … full description “Implementation of biologically inspired efficient deep learning models (available)”
Improving Automatic Bug Detection in JavaScript (completed)
Dynamic symbolic execution (DSE) is an effective tool for bug detection in real software. Like unit testing and fuzzing DSE executes portions of a program, exposing bugs through runtime program exceptions. In DSE, some inputs to the program under test are made “symbolic” while the rest are fixed. Whenever the symbolic execution encounters a conditional operation … full description “Improving Automatic Bug Detection in JavaScript (completed)”
Jupyter notebooks (available)
Prerequisites: experience with Python (useful) and Javascript programming (essential). It may be useful to be willing to learn about functional programming (but this is not essential). Jupyter notebooks [1] are examples of literate programming [2] where code and outputs from the code as well as documentation are in the same application. Jupyter allows the user … full description “Jupyter notebooks (available)”