Software Verification

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



22.11.2011 — New guest speaker on 30.11.2011: Joseph Kiniry.

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

10.08.2011 — 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 of software 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



A few of the Wednesday classes (1 hour, 16-17) are given by guest speakers on a research topic related to the content of the preceding Monday class.

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. 21.09 L1 Overview (BM) Slides
Mon. 26.09 L2 Axiomatic semantics: basics (BM) Slides 09-axiom.pdf
Mon. 26.09 E1 Axiomatic semantics Exercise Solution
Wed. 28.09 L3 Axiomatic semantics: conditionals, loops, etc. (BM)
Mon. 3.10 L4 Axiomatic semantics: procedures, recursion, advanced language constructs (BM)
Mon. 3.10 E2 Axiomatic semantics (continued)
Wed. 5.10 G1 Guest talk: Julian Tschannen (Boogie and OO verification) Slides
Mon. 10.10 L5 Separation logic (SvS) Slides
Mon. 10.10 E3 Verification with Boogie Preparation BPL files Boogie on wine instructions
Wed. 12.10 G2 Guest talk: Cristiano Calcagno (separation logic) Slides
Mon. 17.10 L6 Assertion inference (CAF) Slides
Mon. 17.10 E4 Separation logic Exercise Solution
Wed. 19.10 G3 Guest talk: Nadia Polikarpova (dynamic contract inference) Slides
Mon. 24.10 L7 Proof-carrying code (MN) Slides Example
Mon. 24.10 E5 Separation logic with VeriFast Preparation VeriFast files
Wed. 26.10 E6 Hoare and Separation logic recap Exercise Solution
Mon. 31.10 L8 Data flow analysis (SN) Slides
Mon. 31.10 E7 Data flow analysis Exercise Solution
Wed. 2.11 L9 Data flow analysis – existence of solutions; slicing (SN) Slides
Mon. 7.11 L10 Abstract interpretation (SN) Slides
Mon. 7.11 E8 Slicing; abstract interpretation Exercise Solution
Wed. 9.11 G4 Guest talk: Scott West (SAT and SMT solving) Slides
Mon. 14.11 L11 Model-checking (CAF) Slides
Mon. 14.11 L11 + E9 Model-checking Exercises and solutions
Wed. 16.11 E10 Model-checking exercise (continued)
Mon. 21.11 L12 Software model-checking (CAF) Slides
Mon. 21.11 L12 + E11 Software model-checking Exercise Solution
Wed. 23.11 E12 Software model-checking exercise (continued)
Mon. 28.11 L13 Verification of real-time systems: model-checking with real-time temporal logic (CAF) Slides Exercises
Mon. 28.11 L13 + E13 Verification of real-time systems
Wed. 30.11 G5 Guest talk: Joseph Kiniry (Formal Methods and Elections) Slides
Mon. 5.12 L17 Testing: basics and automated (BM) Slides (parts 1 and 2).
Mon. 5.12 E15 Testing Exercises Solution
Wed. 7.12 G6 Guest talk: Yi Wei (AutoTest) Slides
Mon. 12.12 L18 Testing: test measurements and fault injection (BM) Slides (parts 1 and 2).
Mon. 12.12 E16 Question/answer and problem discussion session
Wed. 14.12 G7 Guest talk: Yu Pei (AutoFix) Slides
Mon. 19.12 Written exam