Software Verification:  2014-2015

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, we discuss hot topics including concurrency, and synthesis.

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. Axiomatic Semantics (Hoare logic, preconditions, postconditions, loop invariants)
3. Models and Operational Semantics (transition systems, CFGs, operational program semantics, soundness/completeness, undecidability)
4. Bounded Model Checking (program unwindings, unwinding assertions, optimisations)
5. Fixed point theory (lattices, monotone functions, fixed points)
6. Abstract Interpretation (abstract domains, abstract fixed points, domain refinement)
7. Concurrency (interleaving semantics, partial-order encoding)
8. Termination (ranking functions, termination as safety property)
9. Synthesis (templates, decision procedures) 

Reading list

• 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

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

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.