Research
The Formal Methods Group is active across a broad range of the subject, from developing the appropriate mathematics for understanding computational systems, through to very practical large-scale specification, verification and system design methods.
System Specification, Verification and Design Methods
We have a large and active group in the development of methods for software and hardware system design, specification and verification, beginning with the work of Professor Cliff Jones, who was a founder member of the group and developed the VDM specification and development methods and associated tools.
Temporal Logics for System Specification and Design
Current activity includes the development of temporal logics for system specification, model-checking and system monitoring, including the Eagle run-time monitoring and verification system.
Research leaders: Howard Barringer and Alan Williams
Component-Based Software Development
Another direction of our activity is in Component-based Software Design which represents a paradigm shift in software development, from building monolithic, single-platform, purpose-built-from-scratch systems to constructing assemblies of ready-made components that are platform-independent and supplied externally. This group undertakes research in all aspects of CBSD, from theoretical foundations, through component models, to tool implementations.
Research leader: Kung-Kiu Lau
Refinement and Retrenchment Methods
Refinement and retrenchment techniques enable computational systems to be developed in a step-wise manner from general functional descriptions in steps to actual implementations. We have developed the theory and applications of these techniques.
Research leader: Richard Banach
Evolvable Systems
An exciting new development lies in the beginnings of an analysis of evolutionary behaviour of systems and the specification and logic of evolvable systems - those whose computational behaviour can be monitored and changed through external agency.
Research leaders: Howard Barringer and David Rydeheard
Automated Reasoning
The mechanisation of logical reasoning has a long history going back at least to the mid-1800s. There is now a world-wide activity in this area with important groups located here in Manchester.Practical and Efficient Automated Reasoning
There is a large group involved in the development of computational systems which will automatically perform logical deduction. One of the main aims of this is to create a very fast and efficient system which is capable of proving complex results in a reasonable time. The output of this is the Vampire system which has repeatedly won in the Conference on Automated Deduction world competition of automated theorem provers.
Research leaders: Andrei Voronkov, Konstantin Korovin, Renate Schmidt, and Tatiana Rybina
Decision and Proof Methods for Modal Logics
We also have a group dedicated to the development and theoretical analysis of proof methods and automated reasoning tools for modal logics and related logics such as description logics.
Research leader: Renate Schmidt
Mathematical Foundations
The Mathematical Foundations Group develops the mathematics which underpins our understanding of computational systems. The relevant mathematics covers logic, especially constructive and other non-standard logics, type theory, topology, abstract algebra (especially category theory), game semantics and recursion theory.
Constructive Set Theories, Logics and Type Theories
The University of Manchester has, through Professor Peter Aczel and his students, a major role in the development of constructive mathematics and type theory. His work covers the foundations of type theories and constructive mathematics, especially set theory and topology. He has developed a constructive version of standard set theory (CZF), engaged in computer-aided proof development tools, and more recently worked on the relationship between set theories and types.
Research leader: Peter Aczel
Semantics and Logics of Computation
Category theory is a branch of mathematics developed from the 1940s onwards as a means of unifying concepts and constructions across many areas of mathematics. More recently it has become a tool to help in the development of the mathematics of computation as it enables us to interpret logics and models of computation. It is also open itself to computation, a fact exploited in the Computational Category Theory system.Research leaders: Andrea Schalk and David Rydeheard
Semantics of Natural Languages
Members of the Formal Methods Group are also involved in developing the semantics of natural languages (such as English), for example in the analysis and processing of texts in the descriptive sciences.
Research leaders: David Rydeheard, David Bree and Mary McGee Wood