Software Verification

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



05.12.2012 — Please remember to bring questions/problems along for the exercise session of next week! The exam is approaching fast now...

22.10.2012 — The project description is now available.

21.08.2012 — 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, 15-16) 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 10:15-12:00 RZ F21
Wednesday 15:15-16:00 RZ F21
Wednesday 16:15-18:00 RZ F21


Date Lecture Title Slides Readings
Wed. 19.09 L1 Overview (BM) Slides
Mon. 24.09 L2 Axiomatic semantics: basics (BM) Slides 09-axiom.pdf
Wed. 26.09 L3 Axiomatic semantics: conditionals, loops, etc. (BM)
Wed. 26.09 E1 Axiomatic semantics Exercise Solution
Mon. 1.10 L4 Axiomatic semantics: procedures, recursion, advanced language constructs (BM) Slides
Wed. 3.10 G1 Guest talk: Julian Tschannen (Boogie and OO verification) Slides
Wed. 3.10 E2 Axiomatic semantics (continued)
Mon. 8.10 L5 Separation logic (SvS) Slides
Wed. 10.10 G2 Guest talk: Cristiano Calcagno (separation logic) Slides
Wed. 10.10 E3 Separation logic Exercise Solution
Mon. 15.10 L6 Assertion inference (CAF) Slides
Wed. 17.10 G3 Guest talk: Nadia Polikarpova (dynamic contract inference) Slides
Wed. 17.10 E4 Verification with Boogie Preparation BPL files
Mon. 22.10 L7 Proof-carrying code (MN) Slides Example
Wed. 24.10 E5 Separation logic with VeriFast Preparation VeriFast files
Wed. 24.10 E6 Hoare and Separation logic recap Exercise Solution
Mon. 29.10 L8 Data flow analysis (SN) Slides
Wed. 31.10 L9 Data flow analysis – existence of solutions; slicing (SN) Slides
Wed. 31.10 E7 Data flow analysis Exercise Solution
Mon. 5.11 L10 Abstract interpretation (SN) Slides
Wed. 7.11 G4 Guest talk: Scott West (SAT and SMT solving) Slides
Wed. 7.11 E8 Slicing; abstract interpretation Exercise Solution
Mon. 12.11 L11 Model-checking (CAF) Slides
Wed. 14.11 L11 Model-checking (continued)
Wed. 14.11 E9 Model-checking Exercises and solutions
Mon. 19.11 L12 Software model-checking (CAF) Slides
Wed. 21.11 L12 Software model-checking (continued)
Wed. 21.11 E10 Software model-checking Exercise Solution
Mon. 26.11 L13 Verification of real-time systems: model-checking with real-time temporal logic (CAF) Slides
Wed. 28.11 L13 Verification of real-time systems (continued)
Wed. 28.11 E11 Verification of real-time systems Exercises
Mon. 3.12 L14 Testing: basics and automated (BM) Slides (parts 1 and 2)
Wed. 5.12 G5 Guest talk: Yu Pei (AutoTest) Slides
Wed. 5.12 E12 Testing Exercises Solution
Mon. 10.12 L15 Testing: test measurements and fault injection (BM)
Wed. 12.12 G6 Guest talk: Ilari Henrik Aegerter, eBay (Testing at eBay)
Wed. 12.12 E13 Question/answer and problem discussion session
Mon. 17.12 Written exam