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: Verification
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)”
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)”
Formal Verification for Blockchains (completed)
In this project you will explore the world of formal verification andblockchains, specifically the new Ethereum 2.0 ‘Proof-of-Stake’ blockchain [1]. This is a more energy-efficient replacement for the original Ethereum ‘Proof-of-Work’ blockchain. As in any blockchain, correctness of thedistributed ‘consensus’ protocol [2] used to maintain the chain and extend it with new blocks is critical. … full description “Formal Verification for Blockchains (completed)”
Formalising Recursive Adaptive Grammars using a Proof Assistant (available)
The aim of this project is to formalise using proof assistant (such as Coq [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)”