Software Verification

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

Course Project

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



23.10.2014 — Please note that the project description has been updated. In particular, the requirement to produce a TEST class and test cases has now been removed.

16.10.2014 — The project description is now online, as well as the skeleton SV_LIST class that you can use as a starting point. Please remember to register your team before 22 October.

25.08.2014 — 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. 17.09 L1 Overview (BM) Slides
Mon. 22.09 L2 Axiomatic semantics: basics (BM) Slides
Wed. 24.09 L3 Axiomatic semantics: conditionals, loops, etc. (BM) Slides
Wed. 24.09 E1 Axiomatic semantics exercises (CP) Problems
Mon. 29.09 L4 Axiomatic semantics: cont. (BM)
Wed. 1.10 G1 Guest talk: Julian Tschannen (AutoProof) Slides
Wed. 1.10 E2 AutoProof exercises (CP) Problems
Mon. 6.10 L5 Separation logic parts I-II (CP) Slides
Wed. 8.10 L5b Separation logic part III (CP) Slides
Wed. 8.10 E3 Separation logic exercises (CP) Problems
Mon. 13.10 L6 Assertion inference (CAF) Slides
Wed. 15.10 G2 Guest talk: Nadia Polikarpova (Boogie) Slides
Wed. 15.10 E4 Boogie exercises (CP) Problems
Mon. 20.10 L7 Separation logic for object-orientation (CP) Slides
Wed. 22.10 L7b Separation logic for object-orientation: continued (CP)
Wed. 22.10 E5 Recap and wrap-up exercises: Hoare logic, separation logic (CP) Problems
Mon. 27.10 L8 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. 29.10 L9 Data flow analysis – existence of solutions; slicing (SN) Slides
Wed. 29.10 E6 Data flow analysis exercises (CP) Problems
Mon. 3.11 L10 Abstract interpretation (SN) Slides
Wed. 5.11 G3 Guest talk: Đurica Nikolić (static analysis / Julia) Slides
Wed. 5.11 E7 Slicing; abstract interpretation exercises (CP) Problems
Mon. 10.11 L11 Model-checking (CAF) Slides
Wed. 12.11 L11 Model-checking (continued)
Wed. 12.11 E8 Model-checking exercises (CP) Problems
Mon. 17.11 L12 Software model-checking (CAF) Slides
Wed. 19.11 L12 Software model-checking (continued)
Wed. 19.11 E9 Software model-checking exercises (CP) Problems
Mon. 24.11 L13 Verification of real-time systems: model-checking with real-time temporal logic (CAF) Slides
Wed. 26.11 L13 Verification of real-time systems (continued)
Wed. 26.11 E10 Verification of real-time systems exercises (CP) Problems
Mon. 1.12 L14 Testing (BM) Slides
Wed. 3.12 G4 Guest talk: Alexey Kolesnichenko (AutoTest) Slides
Wed. 3.12 E11 Testing exercises (CP) Problems
Mon. 8.12 L15 Testing: continued (BM)
Wed. 10.12 G5 Guest talk: Kaue Soares da Silveira, Google (Testing at Google)
Wed. 10.12 E12 Questions, answers, and problem discussion session
Mon. 15.12 Written exam