Date  Topics 
Jul 18 
Introduction and course logistics; notion of program state; programs
as state transition systems; assertion checking as a reachability
problem; notions of abstract and concrete states; importance of
abstractions in program analysis and verification; brief demo of
KeyHoare tool

Jul 21  No class 
Jul 25 
A simple sequential, imperative programming language, sufficiency of
the language for encoding Turing machines, a simple assertion
language. Introduction to Hoare logic: Hoare triples, partial and
total correctness semantics, weakest preconditions and strongest
postconditions and finding them for a simple assignment statement,
Hoare axiom for an assignment statement and its illustration

Jul 28 
Hoare logic inference schema for sequential composition of statements,
conditional statements and loop invariants. Centrality of loop
invariants in analyzing programs with loops, uncomputability of
tightest loop invariants, undecidabilty of checking validity of
arbitrary Hoare triples in our simple languate

Aug 1 
Demonstration of the importance of good loop invariants using Key
Hoare tool: integer division and array sorting. Importance of keeping
all relevant information in an invariant, need for algorithmic
techniques for determining good loop invariants.

Aug 4 
Introduction to the theory of abstract interpretation: powerset
lattice of concrete states, abstract lattice and Galois connection
between the two lattices, properties of Galois connections and their
use in analyzing a program in the abstract domain, alternative
definitions of Galois connection. Computing abstract postcondition
of a statement from the concrete postcondition transformer function,
practical issues with computing the most precise abstract
postcondition and need for overapproximations.

Aug 8  Abstract postcondition of a
sequence of statements and of conditional statements, implications of
representing conditions precisely in abstract domain, viewing a while
loop as a sequence of conditional statements to understand how a loop
invariant may be computed. Formulating an abstract loop invariant as
the limit of a sequence of abstract values, constructing a suitable
map G in the abstract lattice such that the abstract loop invariant is
the limit of G^i(\bot), implications of monotonicity of
G.

Aug 11 
More on the existence of nontrivial abstract loop invariants, their
relation to fixpoints of appropriately constructed maps in the
abstract lattice, prefixpoints, postfixpoints, KnasterTarski
fixpoint theorem. Approximately computing abstract loop invariants:
use of widen operator, properties of widen operator

Aug 18  Inclass KeyHoare based
quiz. More on computing abstract loop invariants: use of widen
operator to get a postfix point, subsequent refining of abstract
loop invariant.

Aug 22  Examples of abstract domains
and corresponding operators: intervals (boxes), defining inclusion,
lub, glb and widen operators on intervals, a general template for
defining widen using thresholds arranged in a lattice with finite height.

Aug 25  The hexagon abstract domain:
Difference Bound Matrices (DBM) and the need to canonicalize them,
allpairs shortest paths for canonicalizing DBMs, inclusion, lub
and glb operators for DBMs

Aug 29  More on hexagons:
interplay of canonicalization and lub/glb computation, widen operator
for hexagons as an extension of corresponding operator for intervals.
Illustrating proving a Hoare triple using intervals and using
hexagons.

Sep 1  Introduction to predicate
abstraction: formulas as domain elements, containment, lub, glb and
widen operators, computing abstract postcondition using predicate
abstraction, introduction to assume and assert statements
and their differences, modeling loops and conditional statements using
assumes, use of overapproximations and underapproximations in different
contexts

Sep 5  More on predicate abstraction,
Constructing a complete Boolean program from a given program and a set
of predicates; equivalence of predicate abstraction on original
program and analysis of boolean state space of Boolean program

Sep 8  Boolean abstractions of programs
with function calls; equivalence of location reachability in pushdown
automata (PDA) and assertion checking in Boolean programs.

Sep 14  Midsemester exam

Sep 19  More on Boolean abstractions of
programs with function calls, illustration by a simple example. Demo
and presentation of CAnalyzer  tool to be used for course projects

Sep 22  Refining Boolean abstraction
of a program by analyzing spurious counterexample traces; discovery of
new predicates; trace formulas and use of Craig interpolation in discovering
new predicates (a nice set of slides can be found here)

Sep 26  Discussion of midsem
solutions. Product operators to combine abstract analyses using
different domains: Cartesian product, reduced product, cardinal power
(a nice set of slides by Prof. Agostino Cortesi can be
found here)

Sep 29  Further discussion of
product operators and their complexity of implementation.
Three ways of refining abstract analysis: product of multiple
abstract domains, refining abstract domain, refining abstract
operators. Illustration of refinement of lub,
glb and widen operators in an abstract domain.
Introduction to bughunting as opposed to proving properties
of programs.

Oct 3  Bounded assertion checking as
a technique to hunt for "shallow" bugs in complex programs; translating
programs without pointers and heap accesses to a system of constraints;
correspondence between models of constraint and assertion violating
traces in the program; keeping size of constraints linear in the size
of the program  difference between tracebased encoding of constraints
and programstructurebased encoding of constraints.

Oct 5  Session on CAnalyzer conducted
by Dr. Hrishikesh Karmarkar and Prateek Saxena. CAnalyzer API
documentation and sample code for the sign domain are
available here.

Oct 6  Further discussion on bounded
assertion checking; translating programs that dereference pointers
and access the heap to systems of constraints using uninterpreted
functions; moving back and forth between error traces in such programs
and models of the generated constraints; dealing with functions with
bounded recursion.

Oct 10  Formulating program verification
as a problem of solving a Horn formula. Illustrating the subtleties
in the formulation.

Oct 13  Discussion on solving Horn
clauses  a few illustrative techniques. Solving Horn clause
formulas with linear inequality templates and Farkas Lemma
(see
the
paper by S. Gulwani, S. Srivastava and R. Venkatesan for
reference).

Oct 17  Introduction to Separation
Logic for reasoning about heap memory manipulating programs;
syntax, semantics and some illustrations of how separating
conjunction and implication enjoy different properties compared to
propositional conjunction and implication. Hoare logic and
separation logic: frame rule

Oct 21  No class. Compensation class on Wed, Oct 25

Oct 24  Representing inductively
defined data structures (e.g. lists, trees) using separation
logic predicates; application of frame rule to prove properties
of programs using separation logic; illustrative examples:
disposing of a tree, maintaining acyclicity of a list, etc. A
nice primer
on separation logic
by Peter
O'Hearn

Oct 25  Using the Frame Rule to
obtain specification of a composition of program fragments from
specifications of individual fragments; biabduction in separation
logic, and its use in inferring specifications of programs from
specifications of components; solving problems using biabduction
and Frame Rule.

Oct 27 
Introduction to threevalued logical structures as an abstraction for
heap, shape graphs, concrete (twovalued) and threevalued structures
and their relation, interpretation of the 1/2 value in threevalued
logic, interpretation of summary predicate, canonical abstraction and
the embedding theorem for threevalued structures. Introduction to
update formulas for threevalued structures with respect to simple
program statements.

Oct 31  Defining update formulas for
threevalued structures with respect to additional program
statements, abstract interpretation using threevalued structures,
illustration through examples. Motivation for focusing
a threevalued structure, focusing threevalued structures for simple
program statements.

Nov 3  More on focusing threevalued
structures with respect to a given formula. Using instrumentation
predicates to infer compatibility conditions, coercing focused
threevalued structures using compatibility condition to improve
the precision of representation.

Nov 7  Practice problem solving using
threevalued logic abstraction of heap. Discussion of quiz 3
solutions. Summarization of course and clarification of doubts.
