Each student is required to do a medium-scale
project as a hands-on exercise in formal verification of programs
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 in due course
of time).
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 individually (no groups).
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.
Useful links for your projects:
- BLAST
code/executable/documentation
- Some "open source software" sources:
- Cross-referenced source
for Linux and some other open source software
- Google Code .
Click on a project label, choose a software and then
click on the "Source" tab to find instructions to checkout
source code.
- Sourceforge.net :
A large open source software repository.
- Freshmeat.net :
An index of Unix and cross-platform software, lots of
them under "open source" license. You should
only use software that has the "free for educational
use" license.
Some more logistics ...
- Midterm and endterm exam, and quizes will be open book, notes and
any material brought to the exam hall.
- If you miss a quiz for a genuine reason, meet the instructor
after setting up an appointment.
- Each quiz will carry equal weightage.
- Informal discussion among students for the purpose of
clarification is strongly encouraged. However, copying solutions from
others will be severely penalized. To understand the distinction
between "copying" and "discussion", please read this.
- 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.
|
Quizzes, Assignments, Practice Problems ...
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
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 (but the PDF/PS slides seem unavailable at the moment).
- Abstract
Interpretation in a Nutshell by Prof. Cousot -- also a must-read to
understand the basics of abstract interpretation.
- 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.
- Refinement in abstract domains like octagons and polyhedra
-
Counterexample driven Refinement for Abstract Interpretation by
Bhargav S. Gulavani and Sriram K. Rajamani,
in Proceedings of International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS), March 2006
-
Automatically Refining Abstract Interpretations by Bhargav S. Gulavani, Supratik Chakraborty, Aditya Nori and Sriram K. Rajamani,
in Proceedings of International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS), March 2008. A journal version containing some proofs omitted in the above paper appears here .
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.
Shape analysis (reasoning about heaps)
-
Regular model checking
-
Three-valued logic analysis
- TVLA home page
- Although we have not covered all topics discussed in the following
papers, the POPL 99 paper is a good introduction to what we have covered
in class. The TOPLAS 02 paper is a much more detailed version for
those interested in additional reading.
References for the more interested ...
- An introductory talk on Hoare Logic
given at Microsoft Research Summer School on Programming Languages,
Analysis and Verification, 2008.
- The Key Project for verifying
Java/JavaCard programs -- a good tool to try out Hoare logic in action.
- Prof. Cousot's
course
on Abstract Interpretation at MIT in Spring 2005.
- Some slides (rather incomplete) used in
class lectures on regular model checking. Please also read sections 7.1 through 7.5 of the
more detailed reference material on this
topic.
|
|