Formal Specification and Verification

Learning Outcomes

Knowledge and Understanding

Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:

• Model checking as an automated technique for verifying properties of software systems
• The use of logical specifications to formalise program correctness
• Refinement-based approaches to program development
• Deductive reasoning techniques for program correctness

Subject Specific Intellectual and Research Skills

Having successfully completed this module you will be able to:

• Understand the workings and limitations of different formal approaches to software correctness
• Capture statements in natural language as formal mathematical statements
• Use a range of verification tools to build correct programs

• Propositional and predicate logic, soundness and completeness (mostly recap)
• Pre- and post-conditions, loop invariants, assertions; program contracts
• Proof calculi for program verification (Hoare logic; dynamic logic)
• Modelling (concurrent) programs using transition systems
• Temporal logic (LTL) and verification by model checking
• Refinement-based approaches to program construction (Event-B)

The content of this module is delivered through lectures, the module website, directed reading, pre-recorded materials and tutorials.

Students work on their understanding through a combination of independent study, preparation for timetabled activities and tutorials, along with formative assessments in the form of coursework assignments.

Summative

This is how we’ll formally assess what you have learned in this module.