Lecturer	Daniel Kroening
Degrees	Schedule C1 — Computer Science Part C — Mathematics and Computer Science Schedule C — MSc in Advanced Computer Science MSc by Research
Term	Hilary Term 2009  (16 lectures)

Overview

The course presents a comprehensive coverage of state-of-the-art practices in software verification. It starts by a brief summary of the basics of Model Checking. We focus on industrial programming languages, that is Java and C/C++, and will discuss techniques for automatic extraction of formal models from these programming languages. We then cover abstract interpretation, bounded model checking, and predicate abstraction.

Learning outcomes

This is a research-oriented course. At the end of the course, the students will

• understand the complexity and sources of complexity in modern programming languages,
• have an in-depth knowledge of modern program analysis techniques,
• be aware of current research challenges in the area.

Prerequisites

A basic understanding of program semantics, automata, and elementary logic will be assumed, for example, as taught in Introduction to the Foundations of Computer Science.

Syllabus

1. Model Checking Basics (transition systems, Kripke structures, paths, reachability, safety/liveness) [1]
2. Model Extraction (parsing, CFGs, typed expression DAGs, semantics) [1]
3. Abstract Interpretation (abstract domains, abstract fixed points, may and must analyses) [1]
4. Bounded Model Checking (unwinding assertions, completeness thresholds) [2]
5. Predicate Abstraction (abstraction with SAT, lazy abstraction, abstraction refinement) [3]
6. Concurrent Software (shared-variable concurrency, concurrent Boolean programs) [2]
7. Compositional Reasoning (assume guarantee, learning environment assumptions) [2]
8. Equivalence Verification (notions of equivalence, inductive reasoning, equivalence with non-programs) [1]
9. Regression Verification (difference slicing, uninterpreted functions) [1]
10. Termination (ranking functions, termination as safety property) [2]

Reading list

• Model Checking, Clarke/Peled/Grumberg, MIT Press 1999
• Decision Procedures, Kroening/Strichman, Springer 2008
  
• Software Reliability Methods, Peled, Springer 2001
• Handbook of Satisfiability, Biere, Heule, Van Maaren, Walsh, IOS Press 2009
• Principles of Model Checking, Baier, Katoen, MIT Press 2008

Related research

Themes	Quantum
Activities	Software Model Checking | Hardware Verification | Model Checking

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.