CS262 15 CATS (7.5 ECTS) Term 2

Availability

Core - CS, CMS; Option - DM

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.

Academic Aims

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.

Learning Outcomes

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.

Content

• 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.

Books

• M.R.A. Huth & M.D. Ryan, Logic in Computer Science: Modelling and reasoning about systems, 2nd edition, Cambridge University Press, 2004.
• D. Jackson, Software Abstractions (revised ed.), MIT Press. 2012
  

Assessment

Two hour examination (75%), coursework (25%)

Teaching

30 lectures and 10 seminars