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

## Automated verification of Rowhammer mitigations (available)

Rowhammer [1], first introduced in [2], is a security exploit that relies on electromagnetic side-effects happening in DRAM memories due to repeated accesses to the same row(s) in a short period of time. In fact, accessing the same row in the DRAM many times in a short span of time may cause electromagnetic interactions with … full description “Automated verification of Rowhammer mitigations (available)”

## Coq Formalisation of Recursive Adaptive Grammars (available)

The aim of this project is to formalise within the Coq proof assistant [1] 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 syntactically correct programs make sense, and … full description “Coq Formalisation of Recursive Adaptive Grammars (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)”

## 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 (available)

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 (available)”