| Module Code | CSU55004 |
| Module Name | Formal Verification |
| ECTS Weighting [1] | 5 ECTS |
| Semester Taught | Semester 1 |
| Module Coordinator/s | Vasileios Koutavas |
Module Learning Outcomes
On successful completion of this module, students will be able to:
- Have gained significant knowledge of mathematical logics (propositional and first order logic) and the Floyd/Hoare logic for software specification. These logics are the basis for software verification, and are a de facto standard in the verification industry;
- Demonstrate the current state-of-the-art in software verification technology, its range of applicability and theoretical limitations, and the necessary tasks required to overcome these limitations where possible;
- Create logic formulas to specify the correct behaviour of programs, including programs implementing well-known algorithms (e.g. binary search), new programs provided to them, and programs they write themselves to solve engineering problems;
- Use the state-of-the-art in software verification tools (e.g. Microsoft Dafny) to mechanically verify software correctness in a team setting;
- Create pencil-and-paper mathematical proofs to manually verify software correctness;
- Design programs that they can then verify correct.
Module Content
Specification languages and logics; axiomatic program semantics. Formal proof systems to verify software and system properties such as propositional, predicate and Hoare logic. Proofs by induction. Correctness proofs of functional and imperative programs.
Teaching and Learning Methods
Lectures, tutorials, individual assignments, projects.
Lectures will be split between presentation of new material and tutorial-style problem solving. Students will have the opportunity to practice the techniques learned in the module, and improve their skills by individual assignments and group project work.
Assessment will be through individual coursework, team project and annual examination.
Assessment Details
| Assessment Component | Brief Description | Learning Outcomes Addressed | % of Total | Week Set | Week Due |
| Examination | 2 hour physical examination | LO1, LO2, LO3, LO4, LO5 | 65% | N/A | N/A |
| Assignment 1 | Propositional Logic | LO1, LO3, LO5 | 4% | Week 3 | Week 4 |
| Assignment 2 | First Order Logic | LO1, LO3, LO5 | 4% | Week 5 | Week 6 |
| Assignment 3 | Hoare Logic/Software Verification | LO1, LO2, LO3, LO4, LO5 | 10% | Week 6 | Week 8 |
| Project Part 1 | Form a Team, Write a Program | LO1, LO2, LO3, LO4, LO5, LO6 | 2% | Week 3 | Week 4 |
| Project Part 2 | Give Formal Spec of Part 1 | LO1, LO2, LO3, LO4, LO5, LO6 | 5% | Week 4 | Week 8 |
| Project Part 3 | Verify Spec of Part 2 | LO1, LO2, LO3, LO4, LO5, LO6 | 10% | Week 8 | Week 11 |
Reassessment Details
Examination 100%, 2 hour physical Examination.
Students must submit a meaningful attempt at least in one of the two assignment and two of the three project parts.
Contact Hours and Indicative Student Workload
| Contact Hours (scheduled hours per student over full module), broken down by: | 22 hours |
| Lecture | 22 hours |
| Laboratory | 0 hours |
| Tutorial or seminar | 0 hours |
| Other | 0 hours |
| Independent study (outside scheduled contact hours), broken down by: | 80 hours |
| Preparation for classes and review of material (including preparation for examination, if applicable) | 40 hours |
| Completion of assessments (including examination, if applicable) | 40 hours |
| Total Hours | 102 hours |
Recommended Reading List
- Main textbook: Logic in Computer Science: Modelling and Reasoning about Systems( 2nd Edition) by Michael Huth and Mark Ryan.
- Lecture notes and handouts.
Module Pre-requisites
Prerequisite modules: N/A
Other/alternative non-module prerequisites: Maths and programming.
Module Co-requisites
N/A