CSU44004 – Formal Verification

Module CodeCSU44004
Module Name Formal Verification
ECTS Weighting[1]5 ECTS
Semester taughtSemester 1
Module Coordinator/s  Vasileios Koutavas

Module Learning Outcomes

On successful completion of this module, students will be able to:

LO1. 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.
LO2. 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.
LO3. 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.
LO4. Use the state-of-the-art in software verification tools (e.g. Microsoft Dafny) to mechanically verify software correctness in a team setting.
LO5. Create pencil-and-paper mathematical proofs to manually verify software correctness.
LO6. 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 ComponentBrief Description Learning Outcomes Addressed% of totalWeek setWeek Due
Examination2 hour take-home examination (available for a 5hr period)LO1, LO2, LO3,
LO4, LO5
65%
Assignment 1Mathematical LogicLO1, LO3, LO58%Week 3Week 6
Assignment 2Hoare Logic/Software
Verification
LO1, LO2, LO3,
LO4, LO5
10%Week 6Week 9
Project Part 1Form a team,
Write a program
LO1, LO2, LO3,
LO4, LO5, LO6
2%Week 2Week 4
Project Part 2Give formal spec of part 1LO1, LO2, LO3,
LO4, LO5, LO6
5%Week 4Week 8
Project Part 3Verify spec of part 2LO1, LO2, LO3,
LO4, LO5, LO6
10%Week 8Week 11

Reassessment Details

Examination 100%; 2 hour take-home examination (available for a 5hr period)

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: 33 hours
Lecture33 hours
Laboratory0 hours
Tutorial or seminar0 hours
Other0 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 Hours113 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:

Other/alternative non-module prerequisites:math, programming

Module Co-requisites

None

Module Website

Blackboard

Guest Links to online lectures:

L02: Wed 15 Sep 2021: https://eu.bbcollab.com/guest/9cd322a1efb54c69a4e35d4522385690

L03: Fri 17 Sep 2021: https://eu.bbcollab.com/guest/499ca43d2542457ab09412df438fb81b