Verification
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.
Research areas 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.
The group has 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.
Core members
Academic staff
- Georg Struth (Head of Group)
- Harsh Beohar
- Kirill Bogdanov
- John Derrick
- Andrei Popescu (affiliate member)
- Mike Stannett
- Jonni Virtema
- Maksim Zhukovskii
- Research 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)