Module overview
This module aims to give a broad introduction to the use of formal methods for proving program correctness.
Aims and Objectives
Learning Outcomes
Knowledge and Understanding
Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:
- The difference between interactive and automated theorem provers and proof methods, in the context of software and system verification
- Major successes and milestones in real-life applications of formal verification, in industry and academia
- The landscape of available methods, tools and programming languages for writing formal specifications of properties of programs
- State-of-the-art methods for verification of functional, imperative and concurrent programs
Subject Specific Intellectual and Research Skills
Having successfully completed this module you will be able to:
- State and verify properties of functional, imperative and concurrent programs
- Assess the strengths and limitations of different formal approaches to software and system correctness
- Develop proofs and programs in a range of verification tools
Syllabus
- Formal specification of properties of programs: basics of declarative programming style, proofs as programs.
- Principles and practices of programming in a general-purpose verification environment (proof assistant): use of propositional, first-order and higher-order syntax, tactic languages, induction principles, automation
- Verification of functional programs: proving function/program equivalence, proving program correctness
- Verification of imperative programs: Hoare logic, program properties involving pre- and post-conditions, and invariants
- Verification of concurrent programs: modelling software systems; temporal logic and verification by model checking.
- Major successes of formal methods in industry and real-life applications: static analysis, formal methods in security, cryptocurrency verification, cyber-physical systems and AI verification.
Learning and Teaching
Teaching and learning methods
The content of this module is delivered through lectures, the module website, directed reading, pre-recorded materials and tutorials.
Students work on their understanding through a combination of independent study, preparation for timetabled activities and tutorials, along with formative assessments in the form of coursework assignments and assessed laboratories.
| Type | Hours |
|---|---|
| Preparation for scheduled sessions | 10 |
| Wider reading or practice | 15 |
| Specialist Laboratory | 20 |
| Revision | 12 |
| Follow-up work | 18 |
| Lecture | 36 |
| Completion of assessment task | 39 |
| Total study time | 150 |
Assessment
Assessment strategy
This module is assessed by a combination of coursework, assessed laboratories, and a final assessment in the form of a written examination.
Summative
This is how we’ll formally assess what you have learned in this module.
| Method | Percentage contribution |
|---|---|
| Laboratory Exercises | 20% |
| Examination | 60% |
| Coursework | 20% |