General
News
18.10.2010 — The description of the course project is now online.
05.10.2010 — Added instructions by Daniel Kroeni for running Boogie on wine.
30.07.2010 — 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 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 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:
- Challenges and issues of verified software.
- The Verification Grand Challenge.
- The role of reuse in software quality; concept of Trusted Components.
- Economic model for reuse-based quality.
- Equipping design patterns with contracts.
- Proving components: Basic Floyd-Hoare-Dikjstra semantics.
- Advanced Floyd-Hoare-Dikjstra semantics: pointers, aliasing.
- Testing components: state of the art in automated testing.
- Static analysis techniques (other than proofs). Flow analysis, slicing.
- Model checking.
Variable topics:
- Separation logic.
- Abstract interpretation.
- Advanced Floyd-Hoare-Dikjstra semantics: inheritance.
- Advanced Floyd-Hoare-Dikjstra semantics: exception handling.
- Advanced Floyd-Hoare-Dikjstra semantics: agents (delegates, function objects).
- The frame problem in software verification.
- Verifying concurrent software (see 251-0268-00L, "Concurrent Object-Oriented Programming").
- Contract inference (e.g. Daikon).
- Program proving environments; case studies of one or two major systems (e.g. Isabelle, Boogie, PVS, ACL2).
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:
- Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis, Springer, ISBN 3-540-65410-0.
- Neil D. Jones, Flemming Nielson: Abstract Interpretation: a Semantic-Based Tool for Program Analysis
Further reading
Axiomatic semantics:
- Robert Floyd: Assigning meanings to programs. Available online, for example here
- C.A.R. Hoare: An axiomatic basis for computer programming. Online, for example here
- Edsger W. Dijkstra: A discipline of programming. Prentice Hall, Eaglewood Cliffs, 1976.
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:
- Several detailed presentations of automata-theoretic model-checking are available from Moshe Vardi; see in particular the one about linear temporal logic.
Real-time modeling and verification:
- A not too technical survey by Furia et al. is available here (ACM Computing Surveys, 42(2):1--59, February 2010).
Previous exams
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 usually be taught by a guest lecturer. 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 | Location |
|---|---|---|
| Monday | 09:00-11:00 | RZ F21 |
| Monday | 13:00-15:00 | IFW A 32.1 |
| Wednesday | 16:00-17:00 | RZ F21 |
Slides
| Date | Lecture | Title | Slides | Readings |
|---|---|---|---|---|
| Wed. 22.09 | L1 | Overview (SN) | Slides | |
| Mon. 27.09 | L2 | Axiomatic semantics: basics (BM) | Slides | 09-axiom.pdf |
| Mon. 27.09 | E1 | Axiomatic semantics | Exercise Solution | |
| Wed. 29.09 | G1 | Axiomatic semantics: introduction to advanced constructs (BM) | ||
| Mon. 4.10 | L3 | Axiomatic semantics: procedures, recursion, advanced language constructs (BM) | Included in L2 slides | |
| Mon. 4.10 | E2 | Verification with Boogie | Preparation BPL files | Boogie on wine instructions |
| Wed. 6.10 | G2 | Guest talk: Julian Tschannen (Boogie and OO verification) | Slides | |
| Mon. 11.10 | L4 | Separation logic (SvS) | Slides | |
| Mon. 11.10 | E3 | Separation logic | Exercise Solution | |
| Wed. 13.10 | G3 | Hoare logic recap | Exercise with solution (with E4) | |
| Mon. 18.10 | L5 | Assertion inference (CAF, BM) | Slides | |
| Mon. 18.10 | E4 | Assertion inference tool demonstrations and Hoare logic recap (cont'd) | Exercises with solution (with G3) | Tools: gin-pink; InvGen. |
| Wed. 20.10 | G4 | Guest talk: Nadia Polikarpova (dynamic contract inference) | Slides | |
| Mon. 25.10 | L6 | Proof-carrying code (MN) | Slides | |
| Mon. 25.10 | E5 | Separation logic with VeriFast | Preparation VeriFast files | |
| Wed. 27.10 | G5 | Guest talk: Cristiano Calcagno (separation logic) | Slides | |
| Mon. 1.11 | L7 | Data flow analysis (SN) | Slides | |
| Mon. 1.11 | E6 | Data flow analysis | Exercise Solution | |
| Wed. 3.11 | G6 | Guest talk: Simon Hudon (design of invariants) | ||
| Mon. 8.11 | L8 | Data flow analysis – existence of solutions; slicing; abstract interpretation – basics (SN) | Slides | |
| Mon. 08.11 | E7 | Slicing; abstract interpretation | Exercise Solution | |
| Wed. 10.11 | G7 | Abstract interpretation – theory (SN) | Slides | |
| Mon. 15.11 | L9 | Model-checking (CAF) | Slides | |
| Mon. 15.11 | E8 | Model-checking | Exercises and solutions | |
| Wed. 17.11 | G8 | Model-checking exercise (continued) | ||
| Mon. 22.11 | L10 | Software model-checking (CAF) | Slides | |
| Mon. 22.11 | E9 | Software model-checking | Exercise Solution | |
| Wed. 24.11 | G9 | Software model-checking exercise (continued) | ||
| Mon. 29.11 | L11 | Verification of real-time systems: model-checking with real-time temporal logic (CAF) | Slides | Exercises |
| Mon. 29.11 | E10 | Software model-checking exercise (continued), project help | ||
| Wed. 1.12 | G10 | Verification of real-time systems II (CAF) | ||
| Mon. 6.12 | L12 | Testing: basics and automated (BM) | Slides | |
| Mon. 6.12 | E11 | Testing | Exercises Solution | |
| Wed. 8.12 | G11 | Guest talk: Yi Wei (AutoTest) | Slides | |
| Mon. 13.12 | L13 | Testing: test measurements and fault injection (BM) | Slides | |
| Mon. 13.12 | E12 | Question/answer and problem discussion session | ||
| Wed. 15.12 | G12 | Guest talk: Yu Pei (AutoFix) | ||
| Mon. 20.12 | Written exam |