- 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 has been 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.]
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.
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.
- 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
Shape analysis (reasoning about heaps) with 3-valued logic
- 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.
Temporal logics for specification
- A wonderful
repository of property specifications using Temporal Logic
- Selected chapters of the book titled Model Checking
by Clarke, Grumberg and Peled, The MIT Press (CFDVS library has
some copies of it -- you can ask your friends in CFDVS to help
you access this book)
- Chapter 3 of Logic in Computer Science: Modeling and Reasoning
about Systems by Michael Huth and Mark Ryan,
Cambridge University Press (since our library has a few copies of this
book, please consider sharing the book if you have issued it).
References for the more interested ...
- An introductory talk on Hoare Logic
given at Microsoft Research Summer School on Programming Languages,
Analysis and Verification, 2008.
- A good set of
slides prepared by Prof. S. Ramesh on material relevant to this course.
- Prof. Cousot's
course
on Abstract Interpretation at MIT in Spring 2005.
- Formal
Methods educational resources from the world-wide web Formal Methods
page.
- The Temporal Logic of Reactive and Concurrent Systems: Specification
by Zohar Manna and Amir Pnueli, Springer Verlag.
- Temporal Verification of Reactive Systems: Safety by Zohar Manna
and Amir Pnueli, Springer Verlag.
|
| Date | Topics details |
|---|
| Jul 25 | Introduction, logistics. A simple
programming language,
examples of some programs in this
language, motivation for formal
reasoning about programs. Notion
of state and configuration of a
program in execution
(process), introduction to operational
semantics of programs. |
| Jul 29 | More on states and configurations of
processes. Configuration transition
graph and operational semantics.
Obtaining transitions in configuration
transition graph for individual statements
in our language.
|
| Aug 1 | Notions of preconditions, postconditions
and terminating computations in configuration
transition graphs.
Use of first-order logic formulae to
represent sets of states in preconditions
and postcoditions.
Informal introduction to Hoare triples and
their partial correctness semantics.
|
| Aug 5 | More on Hoare triples and their partial
and total correctness semantics. Hoare
inference rule schema for assignment
statements, sequential composition of
statements, if-then-else constructs,
and for strengthening preconditions and
weakening postconditions. Illustrations
through examples. |
| Aug 8 | IITB Convocation (no class) |
| Aug 12 | Hoare logic inference rule schema for "while"
loops. Notion of loop invariants and their
use in proving Hoare triple for some interesting
simple programs. Illustration of how a wrong choice of
loop invariants can lead to difficulties in
proving properties of programs. |
| Aug 15 | Independence Day (no class) |
| Aug 19 | Showing that proving Hoare triples even for
a simple programming language is undecidable.
Difficulty of computing strongest loop
invariants. Intuition of what a strongest
loop invariant might look like, and how
overapproximations to that might suffice
for proving Hoare triples. Some
introductory ideas on computing approximate
loop invariants. |
| Aug 22 | Short clarification session by Abhisekh
Sankaran. Class to be compensated later
|
| Aug 26 | Introduction to abstract interpretation,
intuition behind usefulness of good abstract
domains.
Lattices of concrete and abstract states, and
Galois connection between them. Brushup
on basics of lattice theory
|
| Aug 28 | Lattices, monotone functions and fixpoints.
Sketch of Tarski's fixpoint theorem.
Computing a loop invariant as the limit of
a sequence of function compositions.
Least fixpoints and loop invariants as
least fixpoints of appropriately defined
monotone functions.
|
| Aug 29 | Pre-fixpoints, post-fixpoints and fixpoints.
Continuous functions on lattices.
More on Tarski's fixpoint theorem, utility
in invariant computation with finite
abstract lattices.
Mimicking state set transformations in
concrete domain by abstract state
transformations in abstract domain. |
| Sep 2 | Computing exact images and overapproximate
images in the abstract domain.
Relation between abstract least fixpoint
and concrete least fixpoint.
Using the abstract domain and Galois
connection to compute invariants in the
concrete domain. Introduction to the
abstract domain of intervals |
| Sep 5 | Teacher's day function (no class)
|
| Sep 9, 12 | Midsem week (no classes)
|
| Sep 16 | Computing invariants and proving Hoare
triples using an interval abstract
domain of fixed height. Notion of
refining the domain by introducing
additional abstract intervals.
Inadequacy of the interval abstract
domain in proving certain kinds of
program properties. Introduction
to the abstract domain of convex
polyhedra: representation, canonicalization,
lub, glb, partial order relation.
|
| Sep 19 | More on the abstract domain of convex
polyhedra and intervals.
Difficulty of computing fixpoints in
infinite abstract lattices.
Importance of computing post-fixpoints
in the abstract domain in order to
compute invariants. Introduction to
the idea of widening as a technique
to generalize from a pattern in a
chain of lattice elements: simple
widening ideas in the domains of
intervals and convex polyhedra.
|
| Sep 23 | Widening as an operator in a lattice,
utility in computing post-fixpoints of
monotone functions in infinite abstract
lattices, detecting when a post-fixpoint
has been reached when performing widening.
Illustration of computing interesting
loop invariants using polyhedral analysis
and widening. |
| Sep 26 | More on widening: illustration in the
abstract domains of intervals and
convex polyhedra.
Threshold widening, and refining the
quality of invariants by delaying the
widening operation.
Short discussion on narrowing as an
operation to obtain a better invariant
once a post fixpoint has been reached
by widening.
Need for refinement, and motivation
for the abstraction refinement loop.
Non-termination of abstraction refinement
loop in general. Refinement of operations
and abstract domains. Introduction to
the abstract domain of boolean formulae
on a given set of predicates: an easily
refinable abstract domain. |
| Sep 30 | Guest lecture by Bhargav Gulavani:
Introduction to predicate abstraction:
motivation, building abstract configuration
transition graphs from a given program
and a set of predicates, correspondence
between operations on boolean formulae
on predicates and operations on sets of
concrete states, using abstract configuration
transition graphs to prove unreachability
of configurations in programs. Building
abstractions in a lazy manner to gain
efficiency. Brief introduction to Boolean
programs as another way of abstracting
behaviour of programs using a given set
of predicates.
|
| Oct 3 | Guest lecture by Bhargav Gulavani:
Need for refinement: obtaining better
predicates to minimize abstract error
traces that correspond to spurious
counterexamples, motivation for
counterexample-guided abstraction
refinement (CEGAR). Reachability tree
exploration and lazy refinement on
demand. Explosion of predicates
and need for location specific predicates.
Analyzing abstract error traces to
discover location specific predicates:
trace formulae and Craig interpolation,
illustration of how Craig interpolation
yields "succinct", "relevant" location
specific predicates in a CEGAR loop.
|
| Oct 7 | Tutorial 2.
Class to be compensated later |
| Oct 10 | Class cancelled.
Class to be compensated later |
| Oct 14 | Brief recap of predicate abstraction.
Boolean programs as another way to analyze
behaviour of programs using a given set of
predicates. Modeling the behaviour of
Boolean programs with (recursive) function
calls as a push-down automaton (PDA).
Formulating the problem of reachability of a
(location, state) pair in a Boolean program
as the problem of detecting emptiness of
the language recognized by a suitable PDA.
Understanding how assignment statements
in the original program can be modeled by
assignments to predicates in the
corresponding Boolean program, use of
the "?" value in assignments to predicates
to represent non-determinism in the
configuration transition graph of a
Boolean program. |
| Oct 17 | Recap of how assignment statements are
modeled in a Boolean program. Modeling
"if then else" and "while" constructs in Boolean
programs, use of "assert" statement
and modeling its effect. Illustrative
example of translation of a simple program
with a loop to a corresponding Boolean
program, and how the Boolean program
overapproximates the behaviour of the original
program. |
| Oct 21 | Modeling function calls in a Boolean
program. Identifying scopes (global/local)
of predicates in the Boolean program,
identifying parameters of function calls,
computing the values of actual parameters
before invoking a function, and using
predicates updated by the invokved
function to determine values of predicates
in the invoking function. Illustration
through a simple example.
|
| Oct 22 | Further discussion on constructing
Boolean abstractions of programs with
function calls, and recursive function
calls, in particular.
Illustration through an example, of
how properties of recursive functions
can be proved using appropriate Boolean
abstraction. Brief discussion on
counter-example guided refinement.
|
| Oct 24 | A more in-depth discussion of counter-example
guided abstraction refinement in the context
of predicate abstraction. Constructing
abstract counterexamples, and then using them
to derive trace formulae to determine if an
abstract counterexample in spurious. Identifying
relevant predicates from a spurious
counterexample, and using it for refining
predicate abstraction. Illustration
using a straight line piece of code.
|
| Oct 28 | Diwali vacation |
| Oct 31 | Discussion on Craig's Interpolation Theorem,
and its use in discovering location-specific
predicates in counter-example guided
refinement of predicate abstraction.
Illustrations using straight line piece of code,
code with conditionals and loops.
Computing Craig interpolants in some simple
cases of formulas (quantifier-free formulae
involving equalities, disequalities and
inequalities on integer/real variables)
|
| Nov 4 | Computing Craig interpolants in simple
cases of formulas using existential
quantification, Fourier-Motzkin elimination
procedure for systems of linear
inequalities, discussion on alternative
techniques for computing Craig interpolants
and why the method of existential
quantification doesn't always give a
Craig interpolant. Analyzing programs
with pointer variables: notion of heap,
concrete heap graphs and abstract heap
graphs. Using predicates and formulae
on these predicates to represent heap
graphs. |
| Nov 5 | Abstract shape analysis: shape graphs as
an abstraction of concrete heap structures,
use of "may" edges and "must" edges,
use of "summary" nodes,
modeling using three valued predicates,
choice of predicates: unary predicates
corresponding to pointer variables in
program, binary predicates for pointer
valued fields.
Analyzing a program to reverse a linked
list using abstract shape graphs: modeling
the effect of statements manipulating
pointers.
|
| Nov 7 | Abstract shape analysis with unary and binary
predicates, limiting the number of nodes
in abstract shape graph, computing a loop
invariant in terms of abstract shape
graphs. Illustration of how information
about link structures is "blurred" in an
abstract shape graph, as increasing
number of iterations of a while loop are
considered. Discussion on how a given
set of unary and binary predicates may
not suffice to give an abstract shape
graph that is precise enough to prove
properties like acyclicity of lists.
Solving a problem from an ealier question paper
on abstract shape graphs. |
| Nov 11 | Need for richer specification formalisms
than what we have been using so far.
A client-server example and the need
to specify properties that refer to
states in the past and also in the
future. Abstract configuration transition
graphs as Kripke structures, notion
of an infinite path in a Kripke structure,
notion of atomic propositions as facts
of interest.
Introduction to temporal logic operators
U, X, F, G. Discussion on state formulae
and path formulae.
|
| Nov 12 | Use of path quantifiers in obtaining
state formulae from path formulae, and
use of temporal logic operators
U, X, F, G, R for obtaining path formulae
from state formulae. Computation
trees and computation tree logic (CTL):
syntactic restrictions on how path
formulae and state formulae can be
constructed in CTL. Examples of
interesting properties expressed in CTL.
|
| Nov 14 | More discussion on some interesting properties
expressed in CTL, formulae that make intuitive
sense but cannot be expressed in CTL (violate
CTL syntax). Relations between different
CTL formulae. Model checking CTL: techniques
for checking EX, AX, EU, AU formulae on a given
Kripke structure and state, and how these can be
used to check other types of CTL formulae.
Brief summary of topics covered in course and
their relation.
|