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.

A representation of cyberspace.

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

    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)

    Find a PhD

    Search for PhD opportunities at Sheffield and be part of our world-leading research.