Software Verification

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.

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.

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.

1. Model Checking Basics (transition systems, Kripke structures, paths, reachability, safety/liveness) [2]
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 (program unwindings, unwinding assertions, completeness thresholds) [2]
5. Predicate Abstraction (abstraction with SAT, lazy abstraction, abstraction refinement, Craig interpolation) [4]
6. Concurrent Software (shared-variable concurrency, concurrent Boolean programs) [2]
7. Compositional Reasoning (assume guarantee, learning environment assumptions) [2]
8. Termination (ranking functions, termination as safety property) [2]

Model Checking basics, extraction of models from source code, Abstract Interpretation, Bounded Model Checking, predicate abstraction, verification of concurrent software, compositional reasoning, termination.

• Model Checking, Clarke/Peled/Grumberg, MIT Press 1999
  and handouts from 2nd edition
  

• 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