- 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.]
Abstract interpretation, loop invariants, widening, narrowing ...
- A wonderful
tutorial
by Prof. Cousot, explaining in fairly simple language what abstract interpretation
is all about. Highly recommended for everybody taking this course.
- 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.
- Implementation of an Array Bound Checker by N. Suzuki and K. Ishihata, in
Conference Record of the Fourth Annual Symposium on Principles of Programming Languages,
pages 132-143, 1977. This paper talks about a method for computing loop invariants
similar to what we discussed in class.
Boolean programs: A specific case of abstract interpretation
- A beautiful introduction to the paradigm of
Boolean Programs by Tom Ball and Sriram Rajamani
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 ...
- 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 26 | Introduction, logistics. A simple
imperative programming language,
examples of interesting programs in this
language, motivation for formal
reasoning about programs. Using
first-order logic to express
transformations effected by program
statements. |
| Jul 29 | Bonus class on prerequisites: Basics
of first-order logic - syntax,
semantics, undecidability, some
decidable fragments. Basics of automata
theory for finite words - language
acceptance, techniques to answer
questions about emptiness, universality,
language containment. |
| Aug 2 | Prerequisites Quiz |
| Aug 5 | Discussion on program state, and relational
semantics of programs (how programs
transform states). Introduction to Hoare
Logic: syntax, semantics of Hoare
triples. Discussion of how assignment
statements alter program state. Rules
for obtaining weakest pre-condition from
given post-condition, and for obtaining
strongest post-condition from given
pre-condition for assignment statements.
Notions of total and partial correctness
of programs. |
| Aug 6 | Compensation Class: Proving properties
of simple programs with only assignment
statements. Rules for reducing proof
obligations of Hoare triples involving
sequential composition of programs,
if-then-else and while control structures
to proof obligations of simpler Hoare
triples and implications in first-order
logic. Notion of a loop invariant and
its use in proving properties of while
loops. |
| Aug 9 | Proving properties of a simple program with
while, if-then-else, sequential
composition control structures.
Illustration of how knowledge of a loop
invariant can significantly simplify
proving properties of programs.
|
| Aug 12 | Notions of weakest preconditions and
strongest postconditions. Illustration
of the utility of these concepts in
gaining "maximal" information about
intermediate program states in simple
programs. Rules for computing strongest
postconditions and weakest preconditions
for assignment statements, sequential
composition of statements, and
if-then-else control structures.
Discussion on difficulty of computing
weakest preconditions and strongest
postconditions across "while" loops.
|
| Aug 16 | Uncomputability of the strongest loop
invariant of a while loop in an arbitrary
while program: reduction from "halting
problem" of Turing Machines. Using a
recurrence equation to express strongest
pre-condition at the beginning of i'th
iteration of a loop. Discussion on the
limiting solutions to the recurrence
equation. Illustration of use of
recurrence equation through a simple
program. Discussion on difficulty of
obtaining the limiting solution to the
recurrence equation, and the utility of
weaker loop invariants. Connection of loop
invariant computation with computing
fixed points in a suitable lattice.
|
| Aug 19 | More illustration with examples on what is
involved in computing the strongest loop
invariant in a given program.
Connections to fixed point computation in
lattice theory. Continuation of
discussion on lattices, monotone
functions and Tarski's Theorem on fixed
points. |
| Aug 23 | Discussion on two different monotone
functions, such that the strongest loop
invariant is a fixed point of both, but is
the least fixed point (lfp) of one of
them. Advantage of formulating the
strongest invariant as a lfp. Formulating
the lfp as the limit of a sequence of
function applications, starting from the
bottom of the lattice. |
| Aug 26 | Discussion on upper continuous functions.
Computing the lfp of such functions as the
least upper bound of a chain of lattice
elements. Infiniteness of the chain as an
impediment to computing the lfp (strongest
loop invariant). Need for techniques to
compute weaker loop invariants. Discussion
on representing sets of program states
as regions in n-dimensional space, and
using convex upper approximations. |
| Aug 30 | Illustration of the use of the ConvexHull
operator and Widen operator (as used in
Cousot-Halbwachs' 1978 paper) to obtain a
loop invariant of a simple program.
Illustration of the effect of using
widening too early (weak invariants) and
too late (large systems of constraints).
Discussion on representing regions (sets
of program states) by finite sets of
linear inequalities, their advantages and
limitations. |
| Sep 2 | Quiz 1
|
| Sep 6 | More discussion on convex regions and regions
representible by finite sets of linear
inequalities. Comparison of ConvexHull
and Widen operators in terms of extraneous
states included, no. of linear
inequalities used for representation, and
termination issues. Importance of both
operators in finding loop invariants.
Illustration using a simple example.
|
| Sep 9 | Computing a post-fixed point (weaker loop
invariant) using the widening operator.
Tightening the invariant by application of
monotone function to post-fixed points.
Non-termination of the tightening
sequence. Need for a counterpart of
widening, aka "narrowing" to ensure
termination and yet remain restricted to
post-fixed points. Introduction and
discussion on narrowing. |
| Sep 13 | Formal definitions of the narrowing and
widening operators in a complete lattice.
Discussion on two different widening
operators and the corresponding narrowing
operators. |
| Sep 14 | Galois Connection: definitions,
abstraction and concretization functions,
retrospective look at what we've done
being nothing more than operating with a
Galois Connection, relation between lfp
in abstract domain and lfp in concrete
domain, understanding why the widening
and narrowing operators accelerate
progress towards lfp in concrete domain.
Collecting semantics of programs: a
simple example |
| Sep 20 | No class (Mid-semester week)
|
| Sep 23 | No class (Mid-semester week)
|
| Sep 27 | Discussion on collecting
semantics and its use. Abstract
Interpretation: a framework for all we
have done over the past few weeks.
Introduction to Boolean programs.
Discussion on term paper
|
| Sep 30 | More on Boolean programs:
Predicate abstraction, examples.
Model checking and reachability on Boolean
programs
|
| Oct 4 | Location reachability in Boolean programs as
state reachability in push-down automata, discussion
on how to solve this problem; using abstract
traces to construct a system of constraints for
checking feasibility of concrete traces.
Illustration through an example.
|
| Oct 7 | No class |
| Oct 11 | No class |
| Oct 14 | Quiz 2 |
| Oct 18 | Counterexample guided abstraction refinement
of Boolean programs
|
| Oct 20 | Compensation class:
Constructing Boolean programs: issues
involved, use of assert statements,
intuitive translation of assign and assert
statements, role of weakest preconditions
and their underapproximation for a given
set of predicates
|
| Oct 21 | Constructing Boolean abstractions of programs
without function calls: translation of
assign and assert statements, illustration
with an example.
|
| Oct 25 | Constructing Boolean abstractions of programs
with function (including recursive) calls.
Summary of Boolean programs.
Introduction to LTL: syntax and semantics.
|
| Oct 27 | Compensation class:
Illustrative examples of LTL formulae used for
specifying properties of programs. Identities
between LTL operators. Representing sets of
paths satisfying an LTL formula as a regular
language on infinite words. Introduction to
Buchi automata and illustrative examples.
|
| Oct 28 | More on the connection between LTL and
non-deterministic Buchi automata, problems
with a direct Buchi automaton construction,
tableau construction for a given LTL formula
|
| Nov 8 | More on tableau construction,
tableau-based model checking of LTL
specifications.
|
| Nov 10 | Introduction to CTL and CTL model checking.
Summary of topics covered in course.
|