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

Year | MSc |

Prerequisites | N/A |

Term | 1 |

Taught By | James Brotherston, Robin Hirsch, Ilya Sergey, Alexandra Silva, Fabio Zanasi (20% each) |

Aims | The module aims to familiarize students with formal methods for reasoning about transition systems and programs. |

Learning Outcomes | 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.