Language Specifiaction and Program Verification

This research group focuses on mechanised language specification and program verification.

We are currently exploring what it means to build, evaluate, and trust a fully mechanised language specification, using WebAssembly as the real-world example language. This involves developing library specifications which must be robust with respect to the environment: implementations should not leak; and specifications should be useful to the client.

We are also developing compositional program reasoning techniques that scale, leading to both tool-independent foundational theory and automatic tools for verifying properties of programs. In particular, we focus on separation logics and compositional symbolic execution, the formal specification of WebAssembly, and concurrency separation logics.