Each student is required to do a small
project as a hands-on exercise in formal verification of a system.
Each project will involve choosing a code fragment (ideally approx
50-100 lines of uncommented C code) from an open source software, and
verifying some interesting properties of the chosen code fragment
using one of a specified set of tools (to be announced). This will
require modeling the environment of the code fragment appropriately,
and inserting appropriate environmental constraints, where
appropriate. The code fragment and properties must be chosen by
students and approved by the instructor/TA.
Students are required to execute the project in groups of size exactly
one. Each project will be evaluated separately based on a project
report to be submitted prior to end-semester exams, and a live
demonstration of the project according to a schedule to be announced
later.
Some more logistics ...
Midterm and endterm exam, and quizes will be open book, open
notes and any open material brought to the exam hall.
If you miss a quiz for a genuine reason, meet the instructor
as soon as possible after setting up an appointment.
Each quiz will carry equal weightage.
Informal discussion among students for the purpose of
clarification is strongly encouraged.
There will be zero tolerance for dishonest
means like copying solutions from others in quizzes, projects and
end-term exam. Anybody found indulging in such activities will be
summarily awarded an FR grade. The onus will be on the supposed offender
to prove his or her innocence. Please read this to understand the distinction between "copying" and "discussion"
|
Quizzes, Assignments, Practice Problems ...
For some practice problems, please check previous
years' course home pages
|
Reading Material
- Papers, chapters and articles to be announced in class.
- Class notes.
Current Reading List
Propositional and predicate logic prerequisites
- Chapters 1 and 2 of Logic in Computer Science: Modeling
and Reasoning about Systems by Michael Huth and Mark Ryan,
Cambridge University Press
Hoare Logic: Partial correctness proofs
- Chapter 4 of Logic in Computer Science: Modeling and Reasoning
about Systems by Michael Huth and Mark Ryan,
Cambridge University Press
- Sections 1, 2, 3, 4, 5 (upto subsection 5.2.3 and then subsections
5.3.1 and 5.3.2) and 7 (upto subsection 7.3) of Chapter 15,
Methods and Logics for Proving Programs by
P. Cousot, in Handbook of Theoretical Computer Science, Vol B (Formal
Models and Semantics), edited by Jan Van Leeuwen, Elsevier and
The MIT Press
Also available from
Prof. Patrick Cousot's web page.
[You need to read the sections on least fixed point formulations of
loop invariants to follow what will be taught in class. Be advised that
this paper is relatively heavy on notation and requires familiarizing
yourself with notations introduced in Sections 2, 3 and 4 of the paper.]
Abstract interpretation
- A wonderful
tutorial
by Prof. Cousot, explaining in fairly simple language what abstract interpretation
is all about. Highly recommended for everybody taking this course.
- Abstract Interpretation: A Unified Lattice Model for Static Analysis
of Programs by Construction or Approximation of Fixpoints, a classic 1977
paper
by Patrick Cousot and Radhia Cousot.
- Slides (in particular Lecture 15) of a
course
on Abstract Interpretation offered by Prof. Cousot at MIT in Spring 2005.
- Automatic discovery of linear restraints among variables of a program by
P. Cousot and N. Halbwachs, in Conference Record of the Fifth Annual Symposium on
Principles of Programming Languages, pages 84-97, 1978.
A link to the
paper is available from Prof. Cousot's home page. This paper discusses the use of the
widening operator for computing linear invariants.
Boolean programs and predicate abstraction
- A beautiful introduction to the paradigm of
Boolean Programs by Tom Ball and Sriram Rajamani
- BLAST: Berkeley Lazy Abstraction Software Verification Tool
web site is a
must-visit for all students of this course. We will be using this tool
for some of our projects. You should go through the following papers
from the list of papers available at the above web site.
-
Lazy Abstraction by
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre,
Proceedings of the 29th Annual Symposium on Principles of Programming
Languages (POPL), ACM Press, 2002, pp. 58-70.
- Abstractions from Proofs by
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Kenneth L. McMillan,
In ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, 2004.
(You can skim through Section 3 and skip Section 6 of this paper)
-
The Software Model Checker BLAST: Applications to Software Engineering by
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar,
Int. Journal on Software Tools for Technology Transfer, 2007.
References for the more interested ...
- An introductory talk on Hoare Logic
given at Microsoft Research Summer School on Programming Languages,
Analysis and Verification, 2008.
|
Lecture Schedule
Date | Topics details |
Jan 6 | |
|