Note: This module is only available to students in the second year of their degree and is not available as an unusual option to students in other years of study.
To give students an understanding of the basics of mathematical logic, and its applications to specifying and verifying computing systems. Algorithms and proof calculi for verification, as well as associated tools, will be studied. Theory and practice relating to reliability of systems form a vital part of computer science.
On completion of the module the student will be able to:
Construct and reason about proofs in a variety of logics.
- Understand and compare the semantics of a variety of logics.
- Apply logic to specify and verify computing systems.
- Understand basic algorithms for formal verification.
- Use formal verification tools.
Propositional logic: proofs, semantics, normal forms, SAT solvers.
- Predicate logic: proofs, semantics.
- Specifying and modelling software.
- Verification by model checking.
- Proof calculi for program verification.