Software Verification

Bertrand Meyer, Carlo A. Furia, Sebastian Nanz (Fall semester 2009)

 

General info: News | Course description | Grading | Course books | Downloads | Further reading | Exam | Wiki
Lectures: Subjects and Slides


General info

News

14.12.2009 The exam text is now online.
05.10.2009 The description of the course project is now online.
03.07.2009 Course description updated. The material on this page is still subject to revision.
23.06.2009 Website up and running, tentative schedule added.

Course description

Software Verification

Ensuring that software does the right thing takes conisderable 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 ofsoftware 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 ata 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; variable topics.

  1. Required topics.
    1. Challenges and issues of verified software.
    2. The Verification Grand Challenge.
    3. The role of reuse in software quality; concept of Trusted Components.
    4. Economic model for reuse-based quality.
    5. Equipping design patterns with contracts.
    6. Proving components: Basic Floyd-Hoare-Dikjstra semantics.
    7. Advanced Floyd-Hoare-Dikjstra semantics: pointers, aliasing.
    8. Testing components: state of the art in automated testing.
    9. Static analysis techniques (other than proofs). Flow analysis, slicing.
    10. Model checking.
  2. Variable topics
    1. Separation logic.
    2. Abstract interpretation.
    3. Advanced Floyd-Hoare-Dikjstra semantics: inheritance.
    4. Advanced Floyd-Hoare-Dikjstra semantics: exception handling.
    5. Advanced Floyd-Hoare-Dikjstra semantics: agents (delegates, function objects).
    6. The frame problem in software verification.
    7. Verifying concurrent software (see 251-0268-00L, "Concurrent Object-Oriented Programming").
    8. Contract inference (e.g. Daikon).
    9. Program proving environments; case studies of one or two major systems (e.g. Isabelle, Boogie, PVS, ACL2).

Grading

The project (a take-home exercise) will contribute 30% to the overall grade. A written exam on 14 December (during the usual lecture time) will contribute the remaining 70%.

Course books

Model checking:

  • Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2000.

Testing:

  • Mauro Pezzè, Michal Young: Software Testing and Analysis: Process, Principles and Techniques, Wiley, ISBN 0471455938.
  • Paul Ammann, Jeff Offutt: Introduction to Software Testing, Cambridge University Press, ISBN 0521880386.

Program Analysis:

Further reading

Separation logic:

  • A nice and simple introductory paper is available here.
  • For more information, visit the Local Reasoning page of Peter O'Hearn.

Model checking:

Real-time modeling and verification:

  • A not too technical survey by Furia et al. is available here (to appear in ACM Computing Surveys).

Lecture organization

The two weekly sessions of the course will be organized differently:

  • The Monday morning sessions (two hours) are traditional-style lectures, ranging in the course of the semester over the main techniques of software verification.
  • The Wednesday afternoon session (one hour) will be taught by a guest lecturer, usually from another institution. We are happy to have secured the participation of many international experts on software verification. These talks will be accessible to the public --- as a public seminar series (FATS, Formal Approaches To Software) --- in addition to the students of this course, and will be research-oriented, presenting new developments related to the previous Monday's lecture topic.

Attendance in both sessions is required, and the material covered will be subject to questions in the final exam.

Stephan van Staden is the organizing assistant for the course. Please contact him if you have any questions.

Schedule

Day

Time

Room

Monday 9:00-11:00 RZ F21
Monday 13:00-15:00 IFW A 32.1
Wednesday 16:00-17:00 RZ F21 -- Please note that talks may extend until 17:15.

 

Exam

Previous exams:

 

Week by Week Schedule

Date Lecture Title Slides Readings
Wed. 16.09 L1 Overview (BM) PDF
Mon. 21.09 L2 Axiomatic semantics: basics (BM) PDF 09-axiom.pdf
Mon. 21.09 E1 Axiomatic semantics Exercise
Wed. 23.09 G1 Guest: Martin Nordio -- Proof-transforming compilation PDF
Mon. 28.09 L3 Axiomatic semantics: procedures, recursion, advanced language constructs (BM)
Mon. 28.09 E2 Verification with Boogie Preparation BPL files
Wed. 30.09 G2 Guest: Mike Gordon -- Axiomatic semantics and symbolic execution PDF
Mon. 05.10 L4 Separation logic (SvS) PDF Project description
Mon. 05.10 E3 Separation logic with VeriFast Preparation VeriFast files
Wed. 07.10 G3 Guest: Cristiano Calcagno -- Separation logic PDF
Mon. 12.10 L5 Assertion inference (CAF, BM) PDF
Mon. 12.10 E4 Assertion inference tool demonstrations
Wed. 14.10 G4 Guest: Nadia Polikarpova -- Dynamic contract inference PDF
Mon. 19.10 L6 Proof-carrying code (MN or BM) PDF
Mon. 19.10 E5 Recap on Hoare and Separation logic Exercise
Wed. 21.10 G5 Guest: Gilles Barthe -- Proof-carrying code PDF
Thu. 22.10
(IFW E42 17:00-18:00)
G5-bis Guest: Jim Woodcock -- The Verified Software repository PDF
Mon. 26.10 L7 Model-checking (CAF) PDF
Mon. 26.10 E6 Model-checking PDF
Wed. 28.10
(RZ F21 15:00-16:00)
G6-bis Guest: Carroll Morgan -- Program refinement PDF
Wed. 28.10 G6 Guest: Armin Biere -- Bounded model-checking PDF
Mon. 02.11 L8 Software model-checking (CAF) PDF
Mon. 02.11 E7 Software model-checking PDF
Wed. 04.11 G7 Guest: Daniel Kröning -- Software model-checking PDF
Mon. 09.11 L9 Verification of real-time systems: model-checking with real-time temporal logic (CAF) PDF
Mon. 02.11 E8 Real-time verification PDF
Wed. 11.11 G8 Guest: Joel Ouaknine -- Verification of real-time systems PDF
Mon. 16.11 L10 Program analysis: data flow analysis (SN) PDF
Mon. 16.11 E9 Program analysis: data flow analysis Exercise
Wed. 18.11 G9 Guest: Mauro Pezzè -- Program analysis PDF
Mon. 23.11 L11 Program analysis: slicing; abstract interpretation (SN) PDF
Mon. 23.11 E10 Program analysis: slicing; abstract interpretation Exercise
Wed. 25.11 G10 Guest: Patrick Cousot -- Abstract interpretation PDF Programs
Mon. 30.11 L12 Testing: basics & automated (BM) PDF
Mon. 30.11 E11 Testing tools overview
Wed. 02.12 G11 Guest: Jason (Yi) Wei -- Automatic testing PDF
Mon. 07.12 L13 Testing: test measurements & fault injection (BM) PDF
Mon. 07.12 E12 Test coverage measures Exercise
Wed. 09.12 G12 Guest: Andreas Leitner -- The testing process at Google PDF
Mon. 14.12 Written exam