Software Verification
information |
course material
| past exam papers
overview
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.
learning outcomes
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.
prerequisites
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.
synopsis
- Model Checking Basics (transition systems, Kripke structures, paths, reachability, safety/liveness) [2]
- Model Extraction (parsing, CFGs, typed expression DAGs, semantics) [1]
- Abstract Interpretation (abstract domains, abstract fixed points, may and must analyses) [1]
- Bounded Model Checking (program unwindings, unwinding assertions, completeness thresholds) [2]
- Predicate Abstraction (abstraction with SAT, lazy abstraction, abstraction refinement, Craig interpolation) [4]
- Concurrent Software (shared-variable concurrency, concurrent Boolean programs) [2]
- Compositional Reasoning (assume guarantee, learning environment assumptions) [2]
- Termination (ranking functions, termination as safety property) [2]
syllabus
Model Checking basics, extraction of models from source code, Abstract Interpretation, Bounded Model Checking, predicate abstraction, verification of concurrent software, compositional reasoning, termination.
reading list
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
related research at OUCL
|
|