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.

Group members

Verification Group Members

Academic Staff

Kirill Bogdanov
Achim Brucker
John Derrick
Mike Stannett
Georg Struth

Research Staff

Simon Doherty

PhD Students

Mehmet Bakir (Mike Stannett)
George O'Brien (John Derrick)
Michael Foster (John Derrick)
Michael Herzberg (Achim Brucker and Anthony Simons)
Julian Huerta y Munive (Georg Struth)
Marina Ntika (based at SEERC, Mike Stannett and Ioanna Stamatopoulou)
Juan Carlos Saenz Carrasco (Mike Stannett)
Ahmed Sedeeq (Mike Stannett)
Michal Soucha (Kirill Bogdanov)