Each student is required to do a small
project as a handson exercise in formal verification of a system.
Each project will involve choosing a code fragment (ideally approx
50100 lines of uncommented C/C++/Java code) from an open source
software, and verifying some interesting properties of the chosen code
fragment using one (or more) of a set of tools. This will require
modeling the environment of the code fragment appropriately, and
inserting appropriate environmental constraints, where appropriate.
The code fragment and properties must be chosen by students and
approved by the instructor/TA.
Students are required to execute the project in groups of size one.
Each project will be evaluated separately based on a project
report to be submitted prior to endsemester exams, and a live
demonstration of the project.
The project evaluation schedule is as given below. During each of these
evaluations, students must meet the instructor/TA and explain
their project, and also give a demonstration of the project, if asked for.
Deliverables  Date  Where 
Code and properties to be analyzed; abstract domain to be used;
tool(s) to be used; a brief report  Oct 22 
Moodle 
Final report; demonstration of
property verification  Nov 14 
CFDVS Lab 
The following is a tentative list of tools that are
recommended for use in your course project. If you want to use a
different tool, please send an email with the instructor citing
reasons, and set up a meeting to have your choice of tool mutually
approved.
Some more logistics ...
Midterm and endterm exams, and quizes will be open book, open
notes and any open material brought to the exam hall.
If you miss a quiz for a genuine reason, meet the instructor
as soon as possible after setting up an appointment.
Each quiz/tool assignment will carry equal weightage.
Informal discussion among students for the purpose of
clarification is strongly encouraged.
There will be zero tolerance for dishonest
means like copying solutions from others in quizzes, projects and
endterm exam. Anybody found indulging in such activities will be
summarily awarded an FR grade. The onus will be on the supposed offender
to prove his or her innocence. Please read this to understand the distinction between "copying" and "discussion"

Quizzes, Assignments, Practice Problems ...
For some practice problems from previous years, please check previous
years' course home pages. Note that the set of topics taught in earlier years
may vary slightly from those taught in the current offering.

Problem sets for current offering
Reading Material
 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 KeyHoare.
Separation logic in program verification
 John Reynolds' seminal paper
on Separation Logic is an excellent introduction to the topic.
 Hongseok Yang's lecture notes on Program Verification using
Separation Logic at Microsoft Summer School, Bangalore, 2008.
Search for "Microsoft Summer School" and check the links to his
lecture slides (Lectures 0 through 3) at Hongseok's
Talks
page.
 A wonderful
tutorial on Separation Logic given by Peter O'Hearn at CAV 2008.
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.
 Invited talk on "Proving Programs Correct by Abstract Interpretation" at WEPL 2015.
 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 8497, 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
mustvisit 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. 5870.
 Abstractions from Proofs by
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Kenneth L. McMillan,
In ACM SIGPLANSIGACT Conference on Principles of Programming Languages, 2004.
(You can skim through Section 3 and skip Section 6 of this paper)
Program verification using constraint solving
 The CBMC homepage. An excellent set of slides on CBMC are available here.
 A wonderful tutorial on propositional satisfiability solvers and SMT solvers by Roberto Sebastiani.
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.

Lecture Schedule
Date  Topics details 
Jul 19  Introduction to the course; examples of questions
that the course will help answer algorithmically; notion of program state;
programs as (infinite) state transition systems 
Jul 22  Hoare Logic: introduction, Hoare triples, partial and total correctness semantics, assignment axiom 
Jul 26  No class 
Jul 27 (Compensation)  Weakest preconditions
and strongest postconditions, Hoare logic inference rules for
programs with no heap access and no function calls,
proving programs correct using Hoare logic 
Jul 29  Demo of KeyHoare tool; centrality of
loop invariants in proving properties of programs with
loops; illustration of difficulty in guessing right
loop invariants. 
Aug 2  Reduction from the halting problem of Turing
machines to proving assertions in a simple program;
uncomputability of strongest loop invariants;
distinction between loop invariants and inductive loop
invariants; introduction to abstract states for reasoning about
programs 
Aug 5  Duality between concrete state space and
abstract state space, lattice structure of
the concrete space, motivating the abstraction
and concretization operators between the
concrete and abstract state spaces, Galois
connection and its properties, intuitive
motivation of why a Galois connection helps
in reasoning about a program in the abstract
state space. 
Aug 9  Concrete and abstract state transformers (strongest
postcondition calculators).
Formulating the problem of computing a loop
invariant as the limit of a nondecreasing
sequence in the concrete lattice, monotone
maps in a complete lattice and fixed points,
KnasterTarski fixed point theorem, the strongest
loop invariant as a fixed point of an appropriately
defined monotone function.

Aug 12  Recap of the KnasterTarski fixed
point theorem. Continuous (ordertheoretic)
functions, the least fixed
point of a continuous monotone function as the
limit of a nondecreasing sequence starting
from the bottom of a lattice, strongest
loop invariant as the least fixed point of
an appropriately defined continuous monotone
function in the concrete lattice, postfixed
points as (not necessarily strongest) loop
invariants. 
Aug 16  Recap of how a loop innvariant in the concrete
domain is the least fixed point of an appropriate
monotone map in the concrete domain. Mimicking
loop invariant calculations in the abstract domain,
stepwise overapproximations, obtaining an upper
bound of an increasing sequencce using the widen
operator.

Aug 19  Further discussion on the widen operator,
formulating the problem such that it is easy
to detect when a widened sequence has stabilized.
Analyzing a simple program using the interval
abstract domain: abstraction and concretization
operators, partial order relation, lub, glb,
and widen operators, abstract state transformers,
computing an overapproximation of the loop
invariant using the interval abstract domain

Aug 23  Shortcomings of a nonrelational abstract domain
like intervals, Difference Bound Matrices (DBMs)
as a relational extension of intervals, abstraction
and concretization operators, partial
ordering relation, checking for inclusion.
A simple example of using DBMs.

Aug 26  Inclass graded assignment with KeyHoare

Aug 30  Need for canonicalizing DBMs, canonicalizing
using allpairsshortestpaths algorithm,
computing lub, glb and widen with DBMs.

Sep 2  Lecture by Dr. Hrishikesh Karmarkar:
Solving problems using DBMs, intervals and
pairsofintervals abstract domains.

Sep 9  Midsemester exam

Sep 15  Discussion on midsemester exam and inclass KeyHoare assignment

Sep 16  Polyhedra abstract domain and simple
applications; abstract domain operations for polyhedra 
Sep 23  Inclass Quiz 2 
Sep 27  More on the polyhedra domain; need for
counterexample guided refinement when using abstract interpretation;
abstractionrefinement loop; threshold widening
as a refined widening operator 
Sep 30  Hintsbased widening as a refined widening operator;
predicate abstraction and its applications;
Boolean programs and predicate abstraction 
Oct 4  Constructing Boolean programs: modeling assume
statements, and use in ifthenelse and whiledo constructs 
Oct 7  Constructing Boolean programs: modeling assignment statements; an illustrative example from an earlier year's quiz 
Oct 11  Institute Holiday 
Oct 14  Discussion on Quiz2 solutions; modeling function calls in Boolean programs: different possibilities 
Oct 18  Modeling function calls and returns in
Boolean programs; Boolean programs as pushdown automata (PDA);
assertion checking as location reachability in a PDA 
Oct 21  Assertion checking in programs as a
constraint solving problem; translating programs without loops to
constraints; relation between solutions of constraints and
assertionviolating program paths; Inclass Quiz 3

Oct 25  Assertion checking via constraint solving in
programs with loops; translating programs with bounded unwinding of
loops to constraints; detecting when bounding unwinding is sufficient

Oct 28  Using Separation Logic to reason about heaps;
restricted syntax and semantics of Separation Logic, illustrative examples
of use of Separation Logic formulas 
Nov 1  Institute Holiday 
Nov 4  More about semantics of Separation Logic
formulae, use of recursively defined predicates in Separation Logic;
Frame Rule in Hoarestyle reasoning using Separation Logic, example of
an application of Frame Rule. Wrapup of course 
