General
News
05.12.2012 — Please remember to bring questions/problems along for the exercise session of next week! The exam is approaching fast now...
22.10.2012 — The project description is now available.
21.08.2012 — 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 of software 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-Dijkstra semantics.
- Advanced Floyd-Hoare-Dijkstra 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-Dijkstra semantics: inheritance.
- Advanced Floyd-Hoare-Dijkstra semantics: exception handling.
- Advanced Floyd-Hoare-Dijkstra 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, in: Handbook of logic in computer science (vol. 4), Oxford University Press, 1995, ISBN 0-19-853780-8.
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).
- For a broader choice of topics, see the follow-up book (available online from ETH accounts): Furia et al.: Modeling Time in Computing. Springer, 2012.
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.
Stephan van Staden is the organizing assistant for the course. Please contact him if you have any questions.
Schedule
| Day | Time | Location |
|---|---|---|
| Monday | 10:15-12:00 | RZ F21 |
| Wednesday | 15:15-16:00 | RZ F21 |
| Wednesday | 16:15-18:00 | RZ F21 |
Slides
| Date | Lecture | Title | Slides | Readings |
|---|---|---|---|---|
| Wed. 19.09 | L1 | Overview (BM) | Slides | |
| Mon. 24.09 | L2 | Axiomatic semantics: basics (BM) | Slides | 09-axiom.pdf |
| Wed. 26.09 | L3 | Axiomatic semantics: conditionals, loops, etc. (BM) | ||
| Wed. 26.09 | E1 | Axiomatic semantics | Exercise Solution | |
| Mon. 1.10 | L4 | Axiomatic semantics: procedures, recursion, advanced language constructs (BM) | Slides | |
| Wed. 3.10 | G1 | Guest talk: Julian Tschannen (Boogie and OO verification) | Slides | |
| Wed. 3.10 | E2 | Axiomatic semantics (continued) | ||
| Mon. 8.10 | L5 | Separation logic (SvS) | Slides | |
| Wed. 10.10 | G2 | Guest talk: Cristiano Calcagno (separation logic) | Slides | |
| Wed. 10.10 | E3 | Separation logic | Exercise Solution | |
| Mon. 15.10 | L6 | Assertion inference (CAF) | Slides | |
| Wed. 17.10 | G3 | Guest talk: Nadia Polikarpova (dynamic contract inference) | Slides | |
| Wed. 17.10 | E4 | Verification with Boogie | Preparation BPL files | |
| Mon. 22.10 | L7 | Proof-carrying code (MN) | Slides Example | |
| Wed. 24.10 | E5 | Separation logic with VeriFast | Preparation VeriFast files | |
| Wed. 24.10 | E6 | Hoare and Separation logic recap | Exercise Solution | |
| Mon. 29.10 | L8 | Data flow analysis (SN) | Slides | |
| Wed. 31.10 | L9 | Data flow analysis – existence of solutions; slicing (SN) | Slides | |
| Wed. 31.10 | E7 | Data flow analysis | Exercise Solution | |
| Mon. 5.11 | L10 | Abstract interpretation (SN) | Slides | |
| Wed. 7.11 | G4 | Guest talk: Scott West (SAT and SMT solving) | Slides | |
| Wed. 7.11 | E8 | Slicing; abstract interpretation | Exercise Solution | |
| Mon. 12.11 | L11 | Model-checking (CAF) | Slides | |
| Wed. 14.11 | L11 | Model-checking (continued) | ||
| Wed. 14.11 | E9 | Model-checking | Exercises and solutions | |
| Mon. 19.11 | L12 | Software model-checking (CAF) | Slides | |
| Wed. 21.11 | L12 | Software model-checking (continued) | ||
| Wed. 21.11 | E10 | Software model-checking | Exercise Solution | |
| Mon. 26.11 | L13 | Verification of real-time systems: model-checking with real-time temporal logic (CAF) | Slides | |
| Wed. 28.11 | L13 | Verification of real-time systems (continued) | ||
| Wed. 28.11 | E11 | Verification of real-time systems | Exercises | |
| Mon. 3.12 | L14 | Testing: basics and automated (BM) | Slides (parts 1 and 2) | |
| Wed. 5.12 | G5 | Guest talk: Yu Pei (AutoTest) | Slides | |
| Wed. 5.12 | E12 | Testing | Exercises Solution | |
| Mon. 10.12 | L15 | Testing: test measurements and fault injection (BM) | ||
| Wed. 12.12 | G6 | Guest talk: Ilari Henrik Aegerter, eBay (Testing at eBay) | ||
| Wed. 12.12 | E13 | Question/answer and problem discussion session | ||
| Mon. 17.12 | Written exam |