| 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 of a program in execution
(process), reasoning about
programs with variables of finite
type using finite state
transition diagrams,
reasoning about programs with variables
of unbounded type using first-order logic
formulae. |
| Jul 28 | No class.
Compensation class on Sept 2.
|
| Aug 1 | Analyzing assignment statements:
Deriving strongest postcondition from a
given pre-condition, and deriving weakest
pre-condition from a given post-condition.
Dealing with loops: loop invariants and
their role in program proofs. Illustration
using simple examples |
| Aug 4 | Discussion on relational semantics of
programs (how the execution of a
program transforms states)
through the example of a
logarithm-calculating program.
Discussion on the appropriateness of
loop-invariants for proving desired
post-conditions of programs.
Illustration of how loop-invariants
can be carefully strengthened to prove
desired post-conditions. Proof of
correctness of the logarithm-computing
program.
|
| Aug 8 | Formal introduction to Hoare logic: syntax
and semantics. Notions of partial and total
correctness. Axioms and basic inference
rules for partial correctness proofs in
Hoare logic. Relative completeness of
Hoare logic. Discussion on how a brute-force
automated prover can be built for proving
Hoare triples that are semantically true.
Discussion on notions of weakening and
strengthening of constraints (pre- and
post-conditions). |
| Aug 11 | No class due to Convocation.
Compensation class on Sept 2.
|
| Aug 15 | Independence Day |
| Aug 18 | Discussion on strengthening and weakening
of constraints. Weakest pre-conditions
and strongest post-conditions: their
use in Hoare logic proofs.
Discussion on uncomputability of the
strongest loop invariant in sequential
programs: reduction from halting problem
of Turing machines. |
| Aug 22 | Translating programs (with possibly
recursive function calls) manipulating
variables of finite-domain types to
push-down automata. Illustration with
an example. |
| Aug 25 | Analysis of programs with variables of
finite-domain types: reducing proof
obligations in Hoare logic to state
reachability question in an appropriate
push-down automaton (PDA). Reducing
assertion checking in such programs to state
reachability in PDA. Deciding state
reachability in PDA by checking
non-emptiness of an appropriate context-free
language. PDA and CFG based techniques
as an alternative to axioms and inference
rules for proving properties of programs with
finite-domain variables. |
| Aug 29 | Introduction to a C-like language powerful
enough to capture all computation and to
Boolean programs. Motivation and intuition
for translating programs in the former
language to corresponding Boolean programs.
Discussion on semantics preserving syntactic
transformations to aid translation to
Boolean programs. Boolean variables to keep
track of a chosen set of predicates.
Preliminary discussion on translating
assignment statements in original program to
parallel assignments to predicate-tracking
Boolean variables in a Boolean program |
| Sept 1 | Translating procedure call-free programs
in a C-like language to Boolean programs:
discussion on translation of "assert"
statements. Valid traces of a program and
set inclusion relation between traces of
original program and traces of corresponding
Boolean program. Discovering traces of
a Boolean program from corresponding push-down
automaton or context-free grammar. |
Sept 2
(two lectures) | Compensation classes:
More discussion on converting procedure
call-free programs in a C-like language to
Boolean programs. Computing
overapproximations of "assert" conditions in
Boolean programs. Discussion on translation
of assignment statements using weakest
preconditions and underapproximations of
Boolean functions. Illustration of spurious
traces in Boolean programs due to
overapproximation. Detecting spurious
traces by symbolic simulation of trace in
original program and satisfiability solving.
Discovering new predicates to derive a
Boolean program that eliminates a given
spurious trace: illustration through a
simple example. Introductory discussion on
abstraction and counterexample-guided
abstraction refinement framework |
| Sept 5 | Abstract domains other than Boolean
predicates. Notion of collecting semantics
of programs using an abstract domain with a
fixed number of elements, how invariants at
specific program locations can be computed
as appropriate limits of a chain in a
lattice in the abstract domain. Preliminary
discussion on partial orders and lattices.
|
| Sept 8 | Invariants at given program locations as
limiting values of an appropriately defined
sequence of sets, casting computation of the
limit as a least fixpoint computation.
Brief introduction to lattices and
fixpoints, the lattice of sets under
set inclusion. |
| Sept 12 and 15 | No class due to Midsemester week.
Compensation classes on Sept 23 and Oct 14.
|
| Sept 19 | Tarski's theorem on fixpoints. Discussion
on computing invariants at specific program
locations as least fixpoints of
appropriately defined monotone functions.
Approximating least fixpoint computation in
infinite lattices. |
| Sept 22 | Computing invariants, introduction to the
notion of widening, widening as a simple
case of machine learning.
Quiz1 |
| Sept 23 | Compensation class:
Discussion on invariants and inductive invariants.
More examples to illustrate the idea of widening in
computing inductive loop invariants. Learning
patterns of relations between program variables:
using intervals for each variable, using linear
relations between variables. Use of polyhedra
and linear constraints to represent learnt relations
between program variables. Convex hulls and their
use in representing relations between variables.
Illustration of how delaying widening during
loop invariant computation can lead to identification
of stronger inductive loop invariants.
|
| Sept 26 | Introduction to Galois connection and its
usefulness in abstract analysis of programs.
Alternative definitions of Galois connection.
Illustration of Galois connection through
a few examples.
|
| Sept 29 | Discussion on class (non-)performance in
homeworks.
Suprise Quiz2.
Discussion of solutions to quiz2. |
| Oct 3 | More on Galois connections. Concrete and
abstract domains. Mimicking a concrete
domain computation in the abstract domain.
Computing the best abstraction of a
concrete-domain monotone function, using the
abstraction and concretization functions.
|
| Oct 6 | Interesting properties of Galois connections.
Relating computations in the concrete domain
to computations in the abstract domain and
vice versa.
Quiz3
|
| Oct 10 | Discussion of solutions to quiz 3.
Using overapproximations of
abstraction function, lub operator and
the postcondition function in the abstract
domain. Discussion on the effect of this
in computing an overapproximation of the
least fixpoint in the abstract domain.
Illustration of the usefulness of overapproximating
operators in the abstract domain.
|
| Oct 13 | More discussion on overapproximating the
abstract lub operator and the best
abstraction of the concrete postcondition
function.
Revisiting Tarski's theorem: post-fixpoints
and pre-fixpoints.
Relation between concretization of abstract
least fixpoint and concrete least fixpoint
using definition of Galois connection and
Tarski's theorem.
Quiz4
|
| Oct 14 | Compensation class:
Introduction to the general widening operator,
properties of the widening operator. Using
a widened sequence to define am appropriate
function in the abstract domain, such that
the concretization of the least fixpoint of
this function gives an invariant in the concrete
domain. Using the properties of widening to
compute the least fixpoint of this function
in the abstract domain. |
| Oct 17 | More on the general widening operator. Examples
of widening in the interval (or rectangular)
domain and polyhedral domain. Discussion on
the termination clause/finite steps until
convergence of a widened sequence.
Course feedback session |
| Oct 20 | Quiz5
Discussion of solutions to Quiz4. Discussion on how to
abstract a program given a Galois connection
between the concrete and abstract domains. |
| Oct 24 | Diwali vacation |
| Oct 27 | Threshold widening: discussion and specific
examples. Widening operators in the rectangular
(or interval) domain and polyhedral domain
as special cases of threshold widening.
Difficulty of determining when a
general widened sequence has converged.
Specific case of widening for computing
loop invariants: detecting convergence of
the widened sequence deterministically.
Summary of computing weak loop invariants using
abstract interpretation. |
| Oct 31 | Motivation for specifying properties of programs
using efficiently checkable fragments of
first-order logic. Introduction to temporal
logics and Kripke structures: illustration
through examples. Introduction to path and
state formulae, leading to CTL*.
|
| Nov 3 | Introduction to the specification logic CTL*:
syntax and semantics. LTL as a special case
of CTL*. Discussion on what properties can
be conveniently expressed using LTL. Illustration
of usage of LTL.
|
| Nov 7 | More discussion on properties expressed using
LTL; some equivalences between Boolean combinations
of LTL formulae. Some interesting properties
expressed in LTL: illustration through
examples. Introduction to CTL as a special case
of CTL*. Some interesting properties expressed
in CTL: illustration through examples.
|
| Nov 10 | Reducing the number of operators needed to
express CTL formulae. CTL model checking
algorithm: intuition, correctness arguments
and illustration. Summary of contents covered
in course, and their relation to each other.
|