The Formal Methods Group is one of the largest and most active groups within the School of Computer Science and also a major player in the field in the UK and the world.

The group is led by Professor Howard Barringer and includes Professors Peter Aczel and Andrei Voronkov amongst more than a dozen staff and a large number of research students.

The group has a very broad span of interests, ranging from developing the new mathematics of computational behaviour, to the study and development of system design and verification methods. There is a large group dedicated to the automation of logic - Manchester is the home of two world-champion automated theorem-proving systems.

• The world-beating Vampire system for theorem-proving and the principles behind the development of highly efficient fully automated reasoning systems.
• The iProver system - another world champion automated theorem-prover - based on an efficient combination of first-order and ground reasoning.
• Developing and exploiting executable temporal and modal logics, including contributions to the Eagle monitoring logic for hardware and software verification.
• Development of a constructive set theory (CZF) and its relationship to type theories.
• A new technique for developing systems through a relationship called retrenchment and its application to practical system development.
• The development of a logical approach to component-based software design.
• Design and analysis methods for evolvable and adaptive computational systems.
• Models of computational systems and logics based on games.
• Decision and proof methods for a range of modal and description logics.