After successfully taking this course, students will have a theoretical and practical understanding of the principles behind fundamental software verification techniques, including model checking, static analysis, in particular type systems, and theorem proving.

The idea of software verification has been around for decades, but only recently have the techniques become mature enough to be applicable in practice. Key to this success has been (a) combination of previously developed techniques, and (b) automation.

This course embraces this diversity of approaches, by surveying some of the main ideas, techniques, and results in software verification. These include in particular:

• Model checking, which provides efficient techniques for the exhaustive exploration of state-based models of programs and reactive systems.
• Static techniques for program analysis.
• Theorem proving, which, in principle, enables the verification of any program.

To demonstrate some of the techniques in practice, the course will offer two practical projects requiring the application of verification tools to illustrative examples.