The Formal Methods group is a very active group within the School of Computer Science, and is also a major player in the field in both the UK and the world. It is led by Professors Allan Ramsay and Andrei Voronkov.
We have a very broad span of interests, ranging from developing the new mathematics of computational behaviour, through the study and development of system design and verification methods, to all aspects of logic. A lot of work is devoted to the automation of logic: Manchester is the home of the world-champion Vampire theorem-proving system.
- Visit the Formal Methods group webpage.
Automatic theorem proving has a number of important applications, such as Software Verification, Hardware Verification, Hardware Design, Knowledge Representation and Reasoning, Semantic Web, Algebra, and Proving Theorems in Mathematics. Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in computer science.
This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise an advanced theory in practically valuable tools.
Vampire is a theorem prover; a system able to prove theorems. More precisely, it proves theorems in first-order logic. The development of Vampire began in 1994. The current version belongs to the third generation of Vampire.
Vampire has won many awards, including 12 World Championship Titles in Theorum Proving.
Prof Andrei A. Voronkov
A Professor of Formal Methods in the School of Computer Science at The University of Manchester. He is most known for Vampire; an automated theorem prover, the EasyChair conference software and as organiser of the Alan Turing Centenary Conference.
Research interests: Automated Reasoning, Static Analysis of Programs, Software and Hardware Verification, Applications of Computational Logic, Semantic Web Search, Web Services, Semantic Web, Term Indexing and Translation Validation.
- Prof Andrei Voronkov's page.