COMPM086 - 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||COMPM086 (Also taught as COMPGL01)|
|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.|
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:
- Unseen examination (2.5 hrs, 90%)
- 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.