Current students

COMPGL01 - Introduction to Logic, Semantics and Verification

This database contains the 2017-18 versions of syllabuses. Syllabuses from the 2016-17 session are available here.

Note: Whilst every effort is made to keep the syllabus and assessment records correct, the precise details must be checked with the lecturer(s).

CodeCOMPGL01 (Also taught as COMPM086)
Taught ByJames Brotherston, Robin Hirsch, Ilya Sergey, Alexandra Silva, Fabio Zanasi (20% each)
AimsThe module aims to familiarize students with formal methods for reasoning about transition systems and programs.
Learning OutcomesStudents will be able to acquire a sound understanding of various algebras and logics and their application in program reasoning.


Part I: Logic basics

  • Classical propositional & predicate logic.
  • Basic Modal Logic: Kripke frames, Axioms, tableaus.
  • Multimodal logic, Propositional Dynamic Logic.

Part II: Kleene algebra and applications

  • Kleene algebra: basic definitions and semantics.
  • Kleene algebra with tests (KAT).
  • Program analysis using KAT.

Part III: Formal semantics of programming languages

  • Different approaches to formal semantics: operational, denotational and axiomatic semantics.
  • Proofs by induction on derivations and structure.
  • Semantics of programs with computational effects and interaction with the environment (overview).

Part IV: Intro to Separation Logic

  • Logical foundations of separation logic.
  • Inductive definitions.
  • Bunched logic/substructural logic.

Part V: Verification

  • Owicki-Gries and Rely/Guarantee methods.
  • Hoare logics and type theory.
  • Interactive theorem proving.

Method of Instruction

2 hours of lectures per week.


The course has the following assessment components:

  • Coursework (100%)

To pass this course, students must:

  • Obtain an overall pass mark of 50% for all sections combined.


Reading list available via the UCL Library catalogue.