Software Analysis and Verification (CPSC 454 / 554)

Information

Overview

Course Summary

The goal of this course is to introduce the students to the theory and practice of program analysis and software verification.The students will learn the foundations, and through a series of practical exercises, they will experiment with publicly available verification tools.

Course Description

A recent study conducted at the University of Cambridge showed that the global cost of software bugs exceeds $300 billion annually. Companies that produce software that controls aircraft, space shuttles, and medical devices, among others, require modern techniques to ensure the reliability of their products.

In the last decade, software verification has brought forth sophisticated tools that assist software engineers in building reliable software. In this course, we will explore state-of-the-art tools used to automatically decide the correctness of programs, and study the algorithms that power them. Students will learn how to use constraint solvers, decision procedures, SAT solvers, and SMT solvers. There are several approaches to increase software reliability: in this course we focus on verification and the use of formal methods to develop more reliable software.

Software verification aims to prove the correctness of a program with respect to some property. Such properties might include: whether the program will crash, whether it will terminate, or whether the program actually computes what it is supposed to. We will introduce the basic vocabulary of program verification; students will become familiar with assertions, pre- and post-conditions, and inductive invariants. They will learn how to derive mathematical formulas from the code and annotations (so called "verification conditions") and they will implement a verification condition generator.

For program verification to scale, it is crucial to use abstractions to reason about programs. The course will explain the abstract interpretation paradigm. Students will also learn how to use model-checking tools to prove the correctness of programs.

Course Material

There is no compulsory textbook for the course, lecture slides will handed out for each class. However, the students interested in learning more can consult the following books:

• "Principles of Program Analysis" by Flemming Nielson, Hanne R. Nielson and Chris Hankin
• "Model Checking" by Edmund M. Clarke Jr., Orna Grumberg, Doron A. Peled
• "The Calculus of Computaation" by Aaron R. Bradley and Zohar Manna
• "Decision Procedures: An Algorithmic Point of View" by Daniel Kroening and Ofer Strichman

Slides

The slides, recommended reading and other course material are available via Yale's Classes*v2 system.