COMPM088 - Program Verification and Automated Reasoning

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

CodeCOMPM088 (Also taught as COMPGL03)
Taught ByJames Brotherston (100%)
AimsThe module aims to familiarize students with the concepts and techniques currently used by state of the art automated theorem provers and program analysers.
Learning Outcomes

Students will learn the theoretical foundations of automated reasoning, and be able to develop them in applications for program analysis and verification.


This course introduces various formal methods of reasoning about transition systems and programs. The course covers Modal, Temporal and Program Logics as well as algebras of transition systems. Students are taught how to establish complexity bounds on programs and transition systems.

Part I: Automated theorem proving

  • Instantiation based methods
  • First-order resolution with unification
  • DPLL based methods
  • Term rewriting

Part II: Program analysis and verification

  • Model checking
  • Symbolic execution
  • Hoare logic
  • Abstract interpretation
  • Separation logic

Method of Instruction

3 hours of lectures per week and 5 hours of problem classes throughout the term.


The course has the following assessment components:

  • Coursework (10%)
  • Written examination (2.5 hours, 90%)

To pass this course, students must:

  • Obtain an overall pass mark of 50% for all sections combined.
  • Obtain a pass mark of 50% in the written examination.


Reading list available via the UCL Library catalogue.

Further books and other resources will be indicated during the course.