Accessibility statement

Assurance & Proof - COM00170M

« Back to module search

  • Department: Computer Science
  • Module co-ordinator: Dr. Simon Foster
  • Credit value: 20 credits
  • Credit level: M
  • Academic year of delivery: 2024-25

Module summary

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

Module will run

Occurrence Teaching period
A Semester 2 2024-25

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

  • Understand how relational calculus can provide a unifying semantics for different semantic presentations and computational paradigms (real time, concurrency, hybrid systems, probability etc.)

Assessment

Task Length % of module mark
Online Exam -less than 24hrs (Centrally scheduled)
Assurance and Proof		 4 hours 100

Special assessment rules

None

Reassessment

Task Length % of module mark
Online Exam -less than 24hrs (Centrally scheduled)
Assurance and Proof		 4 hours 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


The information on this page is indicative of the module that is currently on offer. The University is constantly exploring ways to enhance and improve its degree programmes and therefore reserves the right to make variations to the content and method of delivery of modules, and to discontinue modules, if such action is reasonably considered to be necessary by the University. Where appropriate, the University will notify and consult with affected students in advance about any changes that are required in line with the University's policy on the Approval of Modifications to Existing Taught Programmes of Study.