Theoretical Computer Science is an area of strength in Electronics and Computer Science (ECS) at Southampton, as highlighted in REF 2021. With the growing impact that computer science has in society and across the economy, there is increased demand for rigorous methods and techniques to model and verify key properties of software systems. From an educational perspective, our degree programmes have a strong theory thread from fundamental discrete and continuous mathematics, through formal methods and theory of computing, to more advanced topics such as automated software verification.
Our work on logic and verification aims to make automated verification the go-to approach in the construction and analysis of software systems, by studying logics and semantic models that can capture the diverse verification needs of modern software, along with verification or synthesis techniques that can scale to large or complex systems. The Software Engineering team work on industrial-strength open source tools for formal design of safety and security critical systems, supported by state-of-the-art automated verification, and underpinned by compositional theories of correctness. Our aim is to strengthen the current and future leadership in theoretical Computer Science and Software Engineering and build further links through to Artificial Intelligence and Cyber Security.
I am an Associate Professor in Computer Science with a research focus on mathematical models and logics for computation. Over the last 15 years I have actively contributed to studying the connection between modal logics and certain general models for dynamical systems known as coalgebras. Just like algebras, coalgebras are simple but fundamental mathematical structures that capture the essence of evolving systems. Through their ability to describe potentially infinite data structures and system behaviour, coalgebras provide a unifying view of many seemingly unrelated concepts, from differential equations to automata theory and process theory, to different flavours of computation, from functional to quantum. While applications of coalgebras are still in their infancy, their potential is huge, given their simplicity, generality and support for reasoning about general dynamics.
I am the Principal Investigator for a three-year Leverhulme Trust Research Project Grant, COalgebraic Foundations for Quantitative VERification, which aims to address current weaknesses in the area of software verification by providing new, systematic foundations based on coalgebras. The project’s vision is that, through their support for compositionality and abstraction, coalgebras hold the key to significantly enhance both the applicability and the scalability of software model checking and synthesis. Systems whose development will benefit from this work include robotic and autonomous systems, which have a need to operate correctly and efficiently in complex environments.