Verified Software

This research group focuses on mechanised language specification and program verification. We are exploring what it means to build, evaluate, and trust a fully mechanised language specification, using JavaScript as the real-world example language. We are 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 developing compositional program reasoning techniques that scale, leading to automatic tools for verifying properties of programs. Our current focus is on modern concurrent separation logics, the development of tools for compositional symbolic analysis using the multi-language platform Gillian, and the specification and verification of Web programs. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course here.