Assurance & Proof - COM00039H

«Back to module search

  • Department: Computer Science
  • Credit value: 20 credits
  • Credit level: H
  • Academic year of delivery: 2023-24

Module summary

This module introduces the mathematical and practical support for the process of software assurance through proof.

Related modules

Pre-requisite modules

Co-requisite modules

  • None

Prohibited combinations

  • None

Module will run

Occurrence Teaching period
A Semester 2 2023-24

Module aims

This module introduces the mathematical and practical support for the process of software assurance through proof. The concepts of inductive data types and recursive functions are covered, and how these can be used to develop the concept of mathematical proof. The module then leads on to contemporary approaches in formal software specification and verification. Methods based on both theorem proving and model checking will be covered using appropriate tools (e.g. Sledgehammer, Nitpick, QuickCheck). Students will learn to apply these techniques to existing programs and systems.

Module learning outcomes

  • Understand and apply interactive theorem proving using the Isabelle proof assistant

  • Compose readable machine-checked proofs using the Isar proof scripting language and proof tactics to execute logical deductions

  • Write and verify functional programs using induction and automated theorem proving in Higher Order Logic

  • Compose formal specifications using pre- and postconditions using relational notations, such as the Z and refinement calculus

  • Reason deductively about programs using notations like Hoare logic and weakest preconditions

  • Develop programs by step-wise refinement through application of refinement laws

Indicative assessment

Task % of module mark
Online Exam -less than 24hrs (Centrally scheduled) 100

Special assessment rules

None

Indicative reassessment

Task % of module mark
Online Exam -less than 24hrs (Centrally scheduled) 100

Module feedback

Feedback is provided through work in practical sessions, and after the final assessment as per normal University guidelines.

Indicative reading

Nikow, T. and Klein, G. Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/

Woodcock J.C.P. and Davies J., Using Z: specification, refinement and proof, Prentice-Hall International, 1996