Each student is required to do a small
project as a hands-on exercise in formal verification of a system.
Each project will involve choosing a code fragment (ideally approx
50-100 lines of uncommented C code) from an open source software, and
verifying some interesting properties of the chosen code fragment
using one of a specified set of tools (to be announced in due course
of time).
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 at least two
and at most three. Each project will be evaluated separately based on
a project report, to be submitted prior to end-semester exams, and a
live demonstration of the project according to a schedule to be
announced later.
Some more logistics ...
Midterm and endterm exam, and quizzes will be open book, notes and
any material brought to the exam hall.
If you miss a quiz for a genuine reason, meet the instructor
after setting up an appointment.
Each quiz 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
end-term 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.
|
Quizzes, Assignments, Practice Problems ...
For some practice problems, please check previous
years' course home pages
[2008, 2007,
2006,
2005, 2004] |
Quiz1 | Fri, Feb 12, 2.00-2.30 pm |
Alternative Quiz1 | Wed, Mar 3, 2.00-2.30 pm |
Midterm Exam | Fri, Feb 19, 2pm |
Homework 1 | Due by Fri, Mar 5, 5pm |
Homework 2 | Due by Fri, Apr 9, 5pm |
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
- 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 will be 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.]
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.
- 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.
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.
- Formal
Methods educational resources from the world-wide web Formal Methods
page.
|
Lecture Schedule
Date | Topics details |
Jan 5 | Introduction and logistics. Brief overview of
reactive and transformative systems, and the need
for specialized specification formalisms.
A simple imperative programming language for
describing transformative systems that operate
on integers. Notion of a state.
A simple assertion language for specifying properties
of states. Semantics of assertions. Introduction
to Hoare logic and Hoare triples. Partial and
total correctness specification of Hoare triples.
Notions of pre- and post-conditions.
|
Jan 8 | Hoare logic proof rules for various statements in
our programming language: assignments, conditional
branches, loop iterations and sequential composition.
Notion of weakest preconditions and strongest
postconditions. Illustration of Hoare logic proof
rules through examples. |
Jan 12 | More discussion on Hoare rule for loop
iteration construct, and the special role of
a "good enough" loop invariant. Inductive
loop invariants, and checking for inductive
invariance. Rules for strengthening
preconditions and weakening postconditions,
and the role of implication in the base
logic in proving validity of a Hoare triple.
Structural rules in Hoare logic.
Illustration of why some of the rules as
studied break when there are shared
resources (like aliased cell allocated on
the heap). Rule of constancy in Hoare logic
and caveats in applying it. Illustration of
proof of correctness of an example program.
|
Jan 15 | No class. Compensation class on Jan 29.
|
Jan 19 | Notion of heap and extended syntax for
programs manipulating heap. Notion of
state for heap manipulating programs.
Introduction to separation logic as a
language for expressing assertions in
programs manipulating heap: basic
predicates on heap, separating conjunction
and separating implication. Semantics of
assertions using separation logic. |
Jan 22 | Partial and total correctness semantics of
Hoare triples for heap manipulating programs.
Hoare-style proof rules using separation
logic for statements allocating heap cells,
freeing heap cells, looking up content of
allocated heap cells, and mutating allocated
heap cells |
Jan 26 | No class (Republic Day) |
Jan 29 | Symbolic heaps and symbolically simulating
programs manipulating heaps.
Recursive predicates (like list(x, y))
using separation logic, and their use in
reasoning about programs manipulating
heaps. Abstracting arbitrarily large
symbolic heaps using recursive predicates.
Illustration through examples of list
manipulating programs.
|
Jan 29
Compensation | Rule of Constancy in Hoare Logic,
Frame Rule of Separation Logic and local
reasoning, applications of frame rule in
modular/local reasoning about programs.
Extending our programming language to
incorporate function calls, illustration
of usage of extended syntax in writing
programs with multiple functions.
|
Feb 2 | No class. Compensation class on Feb 9 |
Feb 5 | Hoare logic rules for function call constructs,
proving Hoare triples for programs with
non-recursive function calls by application of
these rules.
|
Feb 9 | Proving Hoare triples for programs with recursive
function calls, function summaries from base
case of recursion, and from generalization of
successive function summaries. Notion of
concrete states and abstract states, abstraction
as a sound mechanism for reasoning about infinite
state programs. Concrete state transition graphs
and abstract state transition graphs, and their
relations.
|
Feb 9
Compensation | Introduction to the theory of
abstract interpretation. Lattice of sets
of concrete states and lattice of abstract states,
abstraction and concretization functions.
Deriving abstract semantics of program statements
from their concrete semantics. Computing a
loop invariant as the least fixed point of
a suitably defined monotone function in the
lattice of sets of concrete states.
|
Feb 12 | Quiz 1 on proving properties of programs
using Hoare Logic. Discussion of solutions,
and problem solving techniques in Hoare
logic.
|
Feb 16,
Feb 19 | No class -- midsemester examination week
|
Feb 22 | Motivation for Galois connection between
abstract and concrete domains. Some simple
properties of Galois connection that are
useful in comparing results obtained in
concrete domain with corresponding results
in abstract domain. Illustration of the
difficulty of computing a loop invariant in
the concrete domain as the least fixpoint of
a monotone function, motivation for computing
abstract loop invariants.
|
Feb 26 | Computing abstract post-condition and
abstract loop invariants. Abstract loop
invariant as the least fixpoint of an
appropriately defined monotone function in
the abstract domain. Relation between
abstract loop invariant and concrete loop
invariant.
|
|