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).
|Code||COMPGL03 (Also taught as COMPM088)|
|Taught By||James Brotherston (100%)|
|Aims||The module aims to familiarize students with the concepts and techniques currently used by state of the art automated theorem provers and program analysers.|
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.