Methods for the verification of computer hardware and software are among the great success stories of computer science. They are used for proving in mathematically rigorous ways that programs or hardware components function correctly as specified. Our research on verification ranges from the mathematical and logical foundations of programming to practical verification methods and tool support for these. Our strengths include unconventional computing; semantics of concurrent and distributed systems; logics, algebras and formal methods for programs and software systems; grammar inference; verified testing methods; verification of multi-core programs and weak memory models; security verification; interactive and automated theorem proving. More information can be found at the group members' personal web sites.
We have received substantial funding from a number of sources including the European Union, EPSRC, the Royal Society and the London Mathematical Society. Current grants include an EPSRC grant on Verifying Concurrent Algorithms on Weak Memory Models.