- 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
- A deck of slides used in Microsoft Research Summer School 2008. Skip the parts about Separation Logic for now.
- A short note on using KeY-Hoare.
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.
- Introductory slides on "Proving Programs Correct by Abstract Interpretation" .
- 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.
- For those interested in knowing how refinement can be done automatically in
abstract domains like octagons and polyhedra,
this
is an interesting paper to read:
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
Boolean programs and predicate abstraction
- A beautiful introduction to the paradigm of
Boolean Programs by Tom Ball and Sriram Rajamani
- The
CPAChecker site is a
must-visit for all students of this course.
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)
- A wonderful set of slides on the BLAST model checker, by Tom Henzinger, Ranjit Jhala and Rupak Majumdar.
[I'm mirroring the slides here because I can no longer find a link to the original slides.]
Combining abstract interpretaters
- A nice set of slides by Prof. Agostino Cortesi on product operators to combine abstract domains
Survey articles
- A nice survey article on automated techniques for formal software verification by Vijay D'Silva, Daniel Kroening and Georg Weissenbacher.
- Another comprehensive survey article on software model checking (as of 2009) by Ranjit Jhala and Rupak Majumdar.
|