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)
YearMSc
PrerequisitesN/A
Term1
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.

Content

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.

Assessment

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.

Resources

Reading list available via the UCL Library catalogue.