Software Verification

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

Course Project

Here, you will find documents, files, and information relating to the 2013 Software Verification project.

General

News

13.11.2013 — This is to confirm that the course schedule will be changed for all coming Wednesdays, i.e. for the first time on 20.11., as follows: Wednesday 14:15-15:00 (lecture), Wednesday 15:15-17:00 (problem class). This means that both the lecture and the exercise class are shifted and will start one hour earlier than previously. The room will remain the same.

Please also note that, as a one-time exception, the lecture next Monday, 18.11., will take place in IFW C 42 instead of the usual room.

09.10.2013 — The project description is now online, as well as the skeleton SV_LIST class that you can use as a starting point. Please note that:

  1. you must register your team before Tuesday 15th October; and
  2. AutoProof may presently report "segmentation faults" in circumstances when it should not. This is under investigation and will be resolved before Monday 14th October, if not sooner.
Enjoy, and good luck!

29.09.2013 — Schedule revision: (1) the lecture on Monday 30.09 will now be on assertion inference and given by CAF; (2) the lecture on Monday 14.10 will now be given by BM, on a subject to be confirmed closer to the time.

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:

Testing:

Further reading

Axiomatic semantics:

Separation logic:

Model checking:

Real-time modeling and verification:

Previous exams

Lecture

Organization

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.

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

Schedule

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

** except on 18.11, when we'll be in IFW C 42 instead.

Slides and Schedule

Date Lecture Title (Lecturer) Slides Readings
Wed. 18.09 L1 Overview (BM) Slides
Mon. 23.09 L2 Axiomatic semantics: basics (BM) Slides
Wed. 25.09 L3 Axiomatic semantics: conditionals, loops, etc. (BM) Slides
Wed. 25.09 E1 Axiomatic semantics exercises (CP) Problems
Solutions
Mon. 30.09 L4 Assertion inference (CAF) Slides
Wed. 2.10 G1 Guest talk: Julian Tschannen (AutoProof) Slides
Wed. 2.10 E2 AutoProof exercises (CP+Julian) Problems
Classes
AutoProof
Mon. 7.10 L5 Separation logic parts I-II (CP) Slides
Wed. 9.10 G2 Separation logic part III (CP) Slides
Wed. 9.10 E3 Separation logic exercises (CP) Problems
Solutions
Mon. 14.10 L6 Weakest precondition semantics (BM)
Research topic: alias analysis (BM) Slides
Wed. 16.10 G3 Guest talk: Nadia Polikarpova (Boogie and Boogaloo) Slides
Wed. 16.10 E4 Boogie and Boogaloo exercises (CP+Nadia) Problems
Programs
Boogie
Boogaloo
Solutions
Mon. 21.10 L7 Graph-based reasoning and verification (CP) Slides NB: these (optional) readings are quite technical and go beyond what you need for this course.
Wed. 23.10 L7b Graph-based reasoning and verification: continued (CP) (cont.)
Wed. 23.10 E5 Recap and wrap-up exercises: Hoare logic, separation logic, graph-based reasoning (CP) Problems
Solutions
Mon. 28.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. 30.10 L9 Data flow analysis – existence of solutions; slicing (SN) Slides
Wed. 30.10 E6 Data flow analysis exercises (CP) Problems
Solutions
Mon. 4.11 L10 Abstract interpretation (SN) Slides
Wed. 6.11 G4 Guest talk: Đurica Nikolić (static analysis / Julia) Slides
Wed. 6.11 E7 Slicing; abstract interpretation exercises (CP) Problems
Solutions
Mon. 11.11 L11 Model-checking (CAF) Slides
Wed. 13.11 L11 Model-checking (continued) (cont.)
Wed. 13.11 E8 Model-checking exercises (CP) Problems
Solutions
Mon. 18.11
(in IFW C 42)
L12 Software model-checking (CAF) Slides
Wed. 20.11 L12 Software model-checking (continued) (cont.)
Wed. 20.11 E9 Software model-checking exercises (CP) Problems
Solutions
Mon. 25.11 L13 Verification of real-time systems: model-checking with real-time temporal logic (CAF) Slides
Wed. 27.11 L13 Verification of real-time systems (continued) (cont.)
Wed. 27.11 E10 Verification of real-time systems exercises (CP) Problems
Solutions
Mon. 2.12 L14 Testing (BM) Slides
Wed. 4.12 G5 Guest talk: Yu Pei (AutoTest) Slides Tool papers and downloads:
Wed. 4.12 E11 Testing exercises (CP) Problems
Solutions
Mon. 9.12 L15 Testing: continued (BM) (cont.)
Wed. 11.12 G6 Guest talk: Kaue Soares da Silveira, Google (Testing at Google)
Wed. 11.12 E12 Questions, answers, and problem discussion session
Mon. 16.12 Written exam