| 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/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 end-semester 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 |
Tentative list of tools to be used for
project
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
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. 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 Key-Hoare.
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 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.
- 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
must-visit 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. 58-70.
- Abstractions from Proofs by
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Kenneth L. McMillan,
In ACM SIGPLAN-SIGACT 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 pre-conditions
and strongest post-conditions, Hoare logic inference rules for
programs with no heap access and no function calls,
proving programs correct using Hoare logic |
| Jul 29 | Demo of Key-Hoare 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
post-condition calculators).
Formulating the problem of computing a loop
invariant as the limit of a non-decreasing
sequence in the concrete lattice, monotone
maps in a complete lattice and fixed points,
Knaster-Tarski fixed point theorem, the strongest
loop invariant as a fixed point of an appropriately
defined monotone function.
|
| Aug 12 | Recap of the Knaster-Tarski fixed
point theorem. Continuous (order-theoretic)
functions, the least fixed
point of a continuous monotone function as the
limit of a non-decreasing 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, post-fixed
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,
step-wise 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 non-relational 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 | In-class graded assignment with Key-Hoare
|
| Aug 30 | Need for canonicalizing DBMs, canonicalizing
using all-pairs-shortest-paths algorithm,
computing lub, glb and widen with DBMs.
|
| Sep 2 | Lecture by Dr. Hrishikesh Karmarkar:
Solving problems using DBMs, intervals and
pairs-of-intervals abstract domains.
|
| Sep 9 | Mid-semester exam
|
| Sep 15 | Discussion on mid-semester exam and in-class Key-Hoare assignment
|
| Sep 16 | Polyhedra abstract domain and simple
applications; abstract domain operations for polyhedra |
| Sep 23 | In-class Quiz 2 |
| Sep 27 | More on the polyhedra domain; need for
counterexample guided refinement when using abstract interpretation;
abstraction-refinement loop; threshold widening
as a refined widening operator |
| Sep 30 | Hints-based 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 if-then-else and while-do 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 push-down 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
assertion-violating program paths; In-class 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 Hoare-style reasoning using Separation Logic, example of
an application of Frame Rule. Wrap-up of course |
|