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.

A representation of cyberspace.

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

    Research staff

    • Simon Doherty
    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)

    Join our research community

    We are top 5 for research excellence.

    Our research

    PhD opportunities