General
News
22.11.2011 — New guest speaker on 30.11.2011: Joseph Kiniry.
17.10.2011 — The description of the course project is now online.
10.08.2011 — 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
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
A few of the Wednesday classes (1 hour, 16-17) 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 | 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. 21.09 | L1 | Overview (BM) | Slides | |
| Mon. 26.09 | L2 | Axiomatic semantics: basics (BM) | Slides | 09-axiom.pdf |
| Mon. 26.09 | E1 | Axiomatic semantics | Exercise Solution | |
| Wed. 28.09 | L3 | Axiomatic semantics: conditionals, loops, etc. (BM) | ||
| Mon. 3.10 | L4 | Axiomatic semantics: procedures, recursion, advanced language constructs (BM) | ||
| Mon. 3.10 | E2 | Axiomatic semantics (continued) | ||
| Wed. 5.10 | G1 | Guest talk: Julian Tschannen (Boogie and OO verification) | Slides | |
| Mon. 10.10 | L5 | Separation logic (SvS) | Slides | |
| Mon. 10.10 | E3 | Verification with Boogie | Preparation BPL files | Boogie on wine instructions |
| Wed. 12.10 | G2 | Guest talk: Cristiano Calcagno (separation logic) | Slides | |
| Mon. 17.10 | L6 | Assertion inference (CAF) | Slides | |
| Mon. 17.10 | E4 | Separation logic | Exercise Solution | |
| Wed. 19.10 | G3 | Guest talk: Nadia Polikarpova (dynamic contract inference) | Slides | |
| Mon. 24.10 | L7 | Proof-carrying code (MN) | Slides Example | |
| Mon. 24.10 | E5 | Separation logic with VeriFast | Preparation VeriFast files | |
| Wed. 26.10 | E6 | Hoare and Separation logic recap | Exercise Solution | |
| Mon. 31.10 | L8 | Data flow analysis (SN) | Slides | |
| Mon. 31.10 | E7 | Data flow analysis | Exercise Solution | |
| Wed. 2.11 | L9 | Data flow analysis – existence of solutions; slicing (SN) | Slides | |
| Mon. 7.11 | L10 | Abstract interpretation (SN) | Slides | |
| Mon. 7.11 | E8 | Slicing; abstract interpretation | Exercise Solution | |
| Wed. 9.11 | G4 | Guest talk: Scott West (SAT and SMT solving) | Slides | |
| Mon. 14.11 | L11 | Model-checking (CAF) | Slides | |
| Mon. 14.11 | L11 + E9 | Model-checking | Exercises and solutions | |
| Wed. 16.11 | E10 | Model-checking exercise (continued) | ||
| Mon. 21.11 | L12 | Software model-checking (CAF) | Slides | |
| Mon. 21.11 | L12 + E11 | Software model-checking | Exercise Solution | |
| Wed. 23.11 | E12 | Software model-checking exercise (continued) | ||
| Mon. 28.11 | L13 | Verification of real-time systems: model-checking with real-time temporal logic (CAF) | Slides | Exercises |
| Mon. 28.11 | L13 + E13 | Verification of real-time systems | ||
| Wed. 30.11 | G5 | Guest talk: Joseph Kiniry (Formal Methods and Elections) | Slides | |
| Mon. 5.12 | L17 | Testing: basics and automated (BM) | Slides (parts 1 and 2). | |
| Mon. 5.12 | E15 | Testing | Exercises Solution | |
| Wed. 7.12 | G6 | Guest talk: Yi Wei (AutoTest) | Slides | |
| Mon. 12.12 | L18 | Testing: test measurements and fault injection (BM) | Slides (parts 1 and 2). | |
| Mon. 12.12 | E16 | Question/answer and problem discussion session | ||
| Wed. 14.12 | G7 | Guest talk: Yu Pei (AutoFix) | Slides | |
| Mon. 19.12 | Written exam |