Software Verification

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

General info

News

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

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

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 (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.

Schedule

Exam

Previous exams:

• 2009
• 2008
• 2007
• 2006 Solution

Week by Week Schedule