- Department: Computer Science
- Credit value: 20 credits
- Credit level: H
- Academic year of delivery: 2023-24
This module introduces the mathematical and practical support for the process of software assurance through proof.
Pre-requisite modules
Co-requisite modules
- None
Prohibited combinations
- None
Occurrence | Teaching period |
---|---|
A | Semester 2 2023-24 |
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.
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
Task | % of module mark |
---|---|
Online Exam -less than 24hrs (Centrally scheduled) | 100 |
None
Task | % of module mark |
---|---|
Online Exam -less than 24hrs (Centrally scheduled) | 100 |
Feedback is provided through work in practical sessions, and after the final assessment as per normal University guidelines.
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