Software Verification: 2009-2010

Information

Lecturer

Vijay D'Silva | Daniel Kroening

Degrees

Hilary Term — MSc in Computer Science

Part C — Honour School of Mathematics and Computer Science

Part C — Honour School of Computer Science

MSc by Research

Term

Hilary Term 2010 (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. A refresher on programming languages and their semantics follows. The notions of correct programs and bugs are discussed and techniques to find bugs are presented. To show the absence of bugs, a proof of correctness must be produced. Hoare's classic method for reasoning about programs is presented and the inherent difficulty in using this method is shown. The crucial idea in program verification is to use abstraction to reason about programs. 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. The theory of abstraction is called Abstract Interpretation. The analysis methods studied in this course are 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 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

Motivation and Background (propsitional logic, set theory) [2]
Models and Semantics (transition systems, CFGs, program semantics) [2]
Bounded Model Checking (program unwindings, unwinding assertions, optimisations) [2]
Hoare Logic (preconditions, postconditions, loop invariants, undecidability) [1]
Fixed point theory (lattices, monotone functions, fixed points) [2]
Abstract Interpretation (abstract domains, abstract fixed points, may and must analyses) [2]
Predicate Abstraction (automated abstraction, lazy abstraction, refinement, Craig interpolation) [3]
Space of abstractions (combination of abstractions) [1]
Termination (ranking functions, termination as safety property) [2]

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

Related research at OUCL

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