Software Verification

Bertrand Meyer, Carlo A. Furia, Sebastian Nanz, Autumn 2015

Course Project

Here you will find documents, files, and information related to the 2015 Software Verification Project.



24.11.2015Schedule update! There will no longer be a formal exercise class on 25.11. The assistant, however, will be available for questions immediately after the guest lecture. The exercises on testing will be covered during the first half of the class on 2.12; the second half will cover general exam preparation and any further questions you might have.

27.10.2015 — Video lectures from the recent ETH Workshop on Software Correctness and Reliability are now available online. If you're interested in what's going on at the cutting edge of program verification research, they will certainly be worth a look.

07.10.2015 — The project description is now online. Please remember to register your teams before 14th October!

20.07.2015 — A tentative version of the course schedule is now online.

Course objectives

252-0239-00L Software Verification

After successfully taking this course, students will have a theoretical and practical understanding of:

Course description

The idea of software verification has been around for decades, but only recently have the techniques become mature enough to be implemented and be applicable in practice. Progress has been made possible by the convergence of different techniques, originally developed in isolation.

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

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

Course books

Some books are available online using your ETH accounts. Links are provided below where known.

Axiomatic semantics:

Abstract interpretation:

Model checking and real-time:


Further reading

Axiomatic semantics:

Separation logic:

Model checking:

Real-time modeling and verification:

Previous exams



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

Dr. Chris Poskitt (CP) is the organising assistant for the course. Please contact him if you have any questions.


Day Time Location
Monday 10:15-12:00 RZ F 21
Wednesday 14:15-15:00 RZ F 21
Wednesday 15:15-17:00 RZ F 21

Slides, Exercises, and Further Reading

Date Lecture Title (Lecturer) Slides Readings
Wed. 16.09 L1 Overview (BM) Slides
Mon. 21.09 L2 Axiomatic semantics: basics (BM) Slides
Wed. 23.09 L3 Axiomatic semantics: routines, functions, etc. (BM) Slides
Wed. 23.09 E1 Axiomatic semantics exercises (CP) Problems
Mon. 28.09 L4 Weakest preconditions (BM)
Wed. 30.09 L5 Auto-active verification (CP) Slides
Wed. 30.09 E2 Auto-active verification exercises (CP) Problems
Mon. 5.10 L6 Data flow analysis (SN) Slides
  • Nielson et al.: Sections 1.1-1.3, 1.7, 2.1, 2.3, and 2.4 of Principles of Program Analysis (2005)
Wed. 7.10 L7 Data flow analysis: existence of solutions, slicing (SN) Slides
Wed. 7.10 E3 Data flow analysis exercises (CP) Problems
Mon. 12.10 L8 Abstract interpretation (SN) Slides
Wed. 14.10 G1 Guest talk: Scott West, Google (Software Quality at YouTube)
Wed. 14.10 E4 Slicing and abstract interpretation exercises (CP) Problems
Mon. 19.10 L9 Model-checking (CAF) Slides
Wed. 21.10 L10 Model-checking: continued (CAF)
Wed. 21.10 E5 Model-checking exercises (CP) Problems
Mon. 26.10 L11 Software model-checking (CAF) Slides
Wed. 28.10 L12 Software model-checking: continued (CAF)
Wed. 28.10 E6 Software model-checking exercises (CP) Problems
Mon. 2.11 L13 Verification of real-time systems: model-checking with real-time temporal logic (CAF) Slides
Wed. 4.11 L14 Verification of real-time systems: continued (CAF)
Wed. 4.11 E7 Verification of real-time systems exercises (CAF) Problems
Mon. 9.11 L15 Separation logic: part 1 of 2 (CP) Slides
Wed. 11.11 L16 Separation logic: part 2 of 2 (CP) Slides
Wed. 11.11 E8 Separation logic exercises (CP) Problems
Mon. 16.11 L17 Separation logic for object-orientation (CP) Slides
Wed. 18.11 L18 Separation logic for object-orientation: continued (CP)
Wed. 18.11 E9 Program proofs: Hoare logic and separation logic exercises (CP) Problems
Mon. 23.11 L19 Theory of Programs (BM) Slides
Wed. 25.11 G2 Guest talk: Alexey Kolesnichenko (AutoTest) Slides
Wed. 25.11 General Q&A session (no formal exercise sheet)
Mon. 30.11 L20 Testing (BM) Slides
Wed. 2.12 G3 Guest talk: Max (Yu) Pei (AutoFix) Slides
Wed. 2.12 E10 Testing exercises and exam preparation (CP) Problems
Mon. 7.12 L21 Testing: continued (BM)
Wed. 9.12 No exercise session (but office hours available upon request)
Mon. 14.12 Written exam