Formal Methods

Course options and guidance for the Formal Methods topic area

What will I learn from courses in this topic?

Formal methods (FM) is the use of logic and mathematical reasoning to understand the behaviour of dynamic systems in general, and of software and hardware in computer systems in particular. It includes conceptual modelling methods using probability theory and specification languages, process calculi and models of concurrent and distributed systems, formal verification, testing and quality assurance. Thus one can formally prove the correctness and performance of software and hardware systems. This is particularly important for safety critical systems, minimizing resource use in computations and in computer security. The primary aims of the formal methods courses are to introduce students to core concepts of FM, which builds the foundation for the applications of FM in related areas (like Security, Software Engineering and Theoretical Computer Science), as well as possible preparation for PhD study. These courses will be of particular interest to students with a background in either software engineering or mathematics.

What background is typically needed?

Most of the courses will assume a good command of the material in the first two (English or European three-year bachelor's) or three (Scottish or American bachelor's) years of a computer science degree. However, even without such a background, as long as you have a strong mathematical ability and reasonable knowledge, most FM courses can be done.

What courses are available?

Level 11 (MSc) courses:

Types and Semantics for Programming Languages ( 10 credits, Semester 1)

Probabilistic Modelling and Reasoning (20 credits , Semester 2)

Formal Verification (Not delivered in 2022/23).

Level 10 courses:

Automated Reasoning (10 credits, Semester 1)

Software Testing (10 credits, Semester 1)

Software Design and Modelling (20 credits, Semester 2)