Foundations
Formal Methods
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 the world-champion Vampire theorem-proving system.
Some of the major achievements over the last few years are:
- The world-beating Vampire system for theorem-proving and the principles behind the development of highly efficient fully automated reasoning systems.
- 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.
For more details, visit our Research Page, and for access to software tools developed here, our Tools Page.
