Current students

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

CodeCOMPGL03 (Also taught as COMPM088)
YearMSc
PrerequisitesCOMPGL02
Term2
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.

Content

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.

Assessment

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.

Resources

Reading list available via the UCL Library catalogue.