Software Verification

Bertrand Meyer, Carlo A. Furia, Sebastian Nanz, Fall 2010



18.10.2010 — The description of the course project is now online.

05.10.2010 — Added instructions by Daniel Kroeni for running Boogie on wine.

30.07.2010 — Website up and running, tentative schedule added.

Course description

252-0239-00L Software Verification

Ensuring that software does the right thing takes considerable effort, both in applying systematic methods to their construction (a priori) and in assessing the result (a posteriori). Software verification is a booming area of research with considerable import for the software industry.

This course surveys the main approaches to verification with a special focus on the concept of "trusted components": reusable software elements accompanied with a guarantee of quality. Trusted components are a particularly appealing approach to the overall goal ofsoftware quality since the potential for large-scale reuse leverages the verification effort and justifies the investment. From an educational perspective, they provide a microcosm for studying all successful construction and verification techniques at a manageable level of granularity.

As software verification is a rich field with many available techniques, the exact set reviewed may vary from session to session. The present list accordingly has two parts: required topics and variable topics.

Required topics:

Variable topics:

Course books

Model checking:


Program analysis:

Further reading

Axiomatic semantics:

Separation logic:

Model checking:

Real-time modeling and verification:

Previous exams



The two weekly sessions of the course will be organized differently:

Attendance in both sessions is required, and the material covered will be subject to questions in the final exam.

Stephan van Staden is the organizing assistant for the course. Please contact him if you have any questions.


Day Time Location
Monday 09:00-11:00 RZ F21
Monday 13:00-15:00 IFW A 32.1
Wednesday 16:00-17:00 RZ F21


Date Lecture Title Slides Readings
Wed. 22.09 L1 Overview (SN) Slides
Mon. 27.09 L2 Axiomatic semantics: basics (BM) Slides 09-axiom.pdf
Mon. 27.09 E1 Axiomatic semantics Exercise Solution
Wed. 29.09 G1 Axiomatic semantics: introduction to advanced constructs (BM)
Mon. 4.10 L3 Axiomatic semantics: procedures, recursion, advanced language constructs (BM) Included in L2 slides
Mon. 4.10 E2 Verification with Boogie Preparation BPL files Boogie on wine instructions
Wed. 6.10 G2 Guest talk: Julian Tschannen (Boogie and OO verification) Slides
Mon. 11.10 L4 Separation logic (SvS) Slides
Mon. 11.10 E3 Separation logic Exercise Solution
Wed. 13.10 G3 Hoare logic recap Exercise with solution (with E4)
Mon. 18.10 L5 Assertion inference (CAF, BM) Slides
Mon. 18.10 E4 Assertion inference tool demonstrations and Hoare logic recap (cont'd) Exercises with solution (with G3) Tools: gin-pink; InvGen.
Wed. 20.10 G4 Guest talk: Nadia Polikarpova (dynamic contract inference) Slides
Mon. 25.10 L6 Proof-carrying code (MN) Slides
Mon. 25.10 E5 Separation logic with VeriFast Preparation VeriFast files
Wed. 27.10 G5 Guest talk: Cristiano Calcagno (separation logic) Slides
Mon. 1.11 L7 Data flow analysis (SN) Slides
Mon. 1.11 E6 Data flow analysis Exercise Solution
Wed. 3.11 G6 Guest talk: Simon Hudon (design of invariants)
Mon. 8.11 L8 Data flow analysis – existence of solutions; slicing; abstract interpretation – basics (SN) Slides
Mon. 08.11 E7 Slicing; abstract interpretation Exercise Solution
Wed. 10.11 G7 Abstract interpretation – theory (SN) Slides
Mon. 15.11 L9 Model-checking (CAF) Slides
Mon. 15.11 E8 Model-checking Exercises and solutions
Wed. 17.11 G8 Model-checking exercise (continued)
Mon. 22.11 L10 Software model-checking (CAF) Slides
Mon. 22.11 E9 Software model-checking Exercise Solution
Wed. 24.11 G9 Software model-checking exercise (continued)
Mon. 29.11 L11 Verification of real-time systems: model-checking with real-time temporal logic (CAF) Slides Exercises
Mon. 29.11 E10 Software model-checking exercise (continued), project help
Wed. 1.12 G10 Verification of real-time systems II (CAF)
Mon. 6.12 L12 Testing: basics and automated (BM) Slides
Mon. 6.12 E11 Testing Exercises Solution
Wed. 8.12 G11 Guest talk: Yi Wei (AutoTest) Slides
Mon. 13.12 L13 Testing: test measurements and fault injection (BM) Slides
Mon. 13.12 E12 Question/answer and problem discussion session
Wed. 15.12 G12 Guest talk: Yu Pei (AutoFix)
Mon. 20.12 Written exam