Safe and Secure Software Systems – Automated Reasoning for Software Engineering

Software is woven into the fabric of modern life – from communications, entertainment and consumer electronics, to finance, healthcare and national infrastructure.

As well as significant economic and social benefits, the proliferation of software brings with it serious risks – system failures and security vulnerabilities. To combat these risks calls for rigorous methods that enable us to reason precisely about the correctness of a software system. Mathematical logic and formal reasoning provide the foundations for such methods. To be applicable on an industrial scale, however, requires computer assistance in the form of automated tools and techniques.

Our research focuses on the development automated reasoning techniques and their application to verifying the correctness software systems – both at the level of code as well as design. Our industrial collaborators have included Altran Praxis, QinetiQ, BAE Systems, Microsoft Research, D-RisQ and Lemma1.

People: Andrew Ireland, Gudmund Grov, Ekaterina Komendantskaya, Rajiv Murali, Yuhui Lin, Colin Farquhar, Maria Teresa Llano Rodriguez
Projects: DReaM , AI4FM, REMO, PSGraph, Tacny