www.cs.ox.ac.uk/teaching/courses/2010-2011/softwareverification/index.html

You are here:

• Home
• Current Students
• Courses
• Software Verification

Software Verification:  2010-2011

Information

Lecturer	Jade Alglave
Degrees	Schedule C1 — Computer Science Schedule C1 — Mathematics and Computer Science Schedule C — MSc in Computer Science
Term	Hilary Term 2011  (18 lectures)

Overview

The course presents a comprehensive coverage of the foundations and
state-of-the-art in software verification. It begins with a brief
overview of the current need for verification tools. Hoare's classic
method for reasoning about programs is presented to give a first
overview of the concept of verification; the inherent difficulty in
using this method is shown. A more formal account on programming
languages and their semantics follows.  The notions of correct
programs and bugs are discussed and techniques to find bugs are
presented. A crucial idea in program verification is to use
abstraction to reason about programs, known as the theory of abstract
interpretation. Both simple and advanced analyses based on abstraction
will be covered. The advanced analyses are incorporated in industrial
tools and are applied in the development of large systems. Concluding
the course, the notion of modularity in verification is discussed,
focussing on issues that arise with programs that operate on heap;
furthermore, an overview of the field of termination checking is
given.

Learning outcomes

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

• understand the sources of complexity in modern programming languages,
• understand the use of abstraction to cope with intractability of analysis
• have an in-depth knowledge of modern program analysis techniques,
• be aware of current research challenges in the area.

Prerequisites

A basic understanding of sets and relations, logic and program semantics will be assumed. This course is self-contained and any required background knowledge is taught in the lecture or will be covered in the handouts.

Synopsis

1. Motivation and Background (logic, set theory) [2]
2. 
   Axiomatic Semantics (Hoare logic, preconditions, postconditions, loop invariants) [2]
3. 
   Models and Operational Semantics (transition systems, CFGs, operational program semantics, soundness/completeness, undecidability) [2]
4. 
   Bounded Model Checking (program unwindings, unwinding assertions, optimisations) [2]
5. 
   Fixed point theory (lattices, monotone functions, fixed points) [1]
6. Abstract Interpretation (abstract domains, abstract fixed points, may and must analyses) [2]
7. 
   Predicate Abstraction (automated abstraction, lazy abstraction, refinement) [2]
8. 
   Modular Verification and Heap (contracts, invariants, dynamicrames, separation logic) [2]
9. 
   Termination (ranking functions, termination as safety property) [1]
    

 

Reading list

The recommended and required reading material will be drawn from the following sources.

• Model Checking, Clarke/Peled/Grumberg, MIT Press 1999 and handouts from 2nd edition
• Decision Procedures, Kroening/Strichman, Springer 2008
• Handbook of Satisfiability, Biere, Heule, Van Maaren, Walsh, IOS Press 2009
• Principles of Model Checking, Baier, Katoen, MIT Press 2008
• Verifiable Programming, Dahl, Prentice Hall PTR 1992

Related research at the Department of Computer Science

Themes	Foundations, Logic and Structures
Activities	Software Model Checking |  Hardware Verification |  Model Checking