# 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).

Code COMPGL01 (Also taught as COMPM086) MSc N/A 1 James Brotherston, Robin Hirsch, Ilya Sergey, Alexandra Silva, Fabio Zanasi (20% each) The module aims to familiarize students with formal methods for reasoning about transition systems and programs. Students 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.