| 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 two
(three in exceptional cases, with permission from the instructor).
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, members of a group must meet the instructor/TA and explain
their project, and also give a demonstration of the project, if asked for.
| Deliverables | Date | Time | Venue |
|---|
| Group constitution; code and properties to be analyzed;
tool(s) to be used; a brief report | Wed, Oct 7 |
3pm - 6pm |
CFDVS Lab |
| Final report; demonstration of
property verification | Wed, Nov 4 |
2.30pm - 6pm |
CFDVS Lab |
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 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, please check previous
years' course home pages
|
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.
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.
- Invited talk on "Proving Programs Correct by Abstract Interpretation" at WEPL 2015.
- 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)
Shape analysis (reasoning about heaps) with 3-valued logic
Although we have not covered all topics discussed in the following
papers, the POPL 99 paper is a good introduction to what we have covered
in class. The TOPLAS 02 paper is a much more detailed version for
those interested in additional reading.
- Parametric Shape Analysis
via 3-valued Logic by M. Sagiv, T. Reps and R. Wilhelm, in Proceedings
of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(POPL), 1999
- Parametric Shape
Analysis via 3-valued Logic by M. Sagiv, T. Reps and R. Wilhelm,
in ACM Transactions on Programming Languages and Systems (TOPLAS),
Vol. 24, Number 3, 2002.
- An excellent set of slides on TVLA from T. Reps, M. Sagiv and R. Wilhelm.
[I'm mirroring the slides here because I can no longer find a link to the original slides on the web.]
Program verification using constraint solving
- The CBMC homepage. An excellent set of slides on CBMC are available here.
- A few slides on Tseitin encoding prepared by the instructor.
- A wonderful tutorial on propositional satisfiability solvers and SMT solvers by Roberto Sebastiani.
- A tutorial on software model checking with Horn clauses. Note that not all material in the tutorial was covered in the course.
- Another tutorial that deals with software verification using Horn clauses. Note again that we haven't covered all material in this tutorial in the course.
- Ashutosh Gupta's slides on SMT solving and interpolant generation.
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 20 | No class |
| Jul 23 | No class |
| Jul 27 | Introduction to the course; basics of Hoare
logic and Hoare triples; Hoare inference rules for assignment
statements and sequential composition, using implications to derive
new Hoare triples from existing ones |
| Jul 30 | Hoare inference rules for if-then-else and
while-do statements; importance and difficulty of computing loop
invariants; proving a Hoare triple involving an iterative program
using Hoare inference rules, uncomputability of strongest post
conditions in integer programs with while loops. |
| Jul 31 | Notion of a program state and sets of
states; program statements as state set transformers; difficulty of
reasoning with sets of concrete states; using an abstract lattice of
state sets for reasoning |
| Aug 3 | Abstract interpretation: Basics of lattice
theory and Galois connections, simple relations implied by the
definition of a Galois conneciton; intuitive idea of analyzing a
program in the abstract domain using a Galois connection with the
concrete domain |
| Aug 6 | Abstract interpretation: Programs as
transformers of state sets, concrete and abstract state transformers
and relations between them; illustration using the abstract domain of
intervals (or boxes) |
| Aug 7 | Abstract interpretation: taking a closer look
at while loops; loop invariants as the limit of an increasing sequence
of subsets (or abstract elements) |
| Aug 10 | Using results from lattice theory to
characterize loop invariants: Knaster-Tarski fixed point theorem,
Kleene fixed point theorem, loop invariant as the least fixed point
of an appropriately defined function |
| Aug 13 | Approximating loop invariants in the abstract
domain: pre- and post-fix points and their properties, widen operator
in an abstract lattice and computing over-approximations of loop
invariants |
| Aug 17 | Detailed look at widen operator, using
widen to compute loop invariants as post-fixpoints in the abstract
lattice, illustration of complete abstract interpretation flow using
interval domain on a simple program |
| Aug 20 | The polyhedra abstract domain for programs
with numeric variables |
| Aug 24 | The octagon abstract domain for programs
with numeric variables; discussion of quiz question from earlier year
|
| Aug 27 | More on quiz solution from earlier year.
Predicate abstraction and Boolean programs: illustrating utility of
Boolean programs in program verification. |
| Aug 31 | Constructing Boolean programs from a given
program and set of predicates; understanding how expandng or shrinking
the set of predicates affects the precision of analysis using a Boolean
program; equivalence of assertion checking and control (error) location
reachability |
| Sep 3 | Finding a good set of predicates for predicate
abstraction; use of Craig interpolants for predicate-hunting; in-class
quiz 2
reachability |
| Sep 15 | Mid-semester examination |
| Sep 21 | Discussion of mid-semester exam solutions;
brief introduction to separation logic for reasoning about memory accesses;
semantics of separating conjunction and implication; proving properties of
programs manipulating linked lists using separating conjunction
|
| Sep 24 | More on using separation logic as the base
logic in Hoare-style reasoning; use of separating implication in proving
properties of programs; properties of separating conjunction vis-a-vis
logical conjunction |
| Sep 28 | Example of Hoare triples using separtion
logic; abstract interpretation for reasoning about healps using
three-valued logic: introduction, formulas and structures, core and
instrumentation predicates; update formulas for core and instrumentation
predicates |
| Oct 1 | Illustration of heap-related property
verification using three-valued logic analysis; focusing a three-valued
structure with respect to a formula, and its uses |
| Oct 5 | Discussion on class project; illustration
of property verification of a program with loops and conditionals
using the domain of octagons |
| Oct 8 | Assertion checking in loop-free programs by
reduction to constraint solving; discussion on nature of constraints;
modeling pointer dereferences using uninterpreted functions | |
| Oct 12 | Closer look at constraints for assertion
checking in a loop-free program; importance of mapping constraint
solutions to program states and vice versa; implications of a few
alternative constraint formulations |
| Oct 15 | Bounded assertion checking in programs with
loops by reduction to constraint solving; formulation of unwinding
assertions |
| Oct 19 | Illustrating use of Z3 as a constraint solver
for proving program properties |
| Oct 26 | Modeling program semantics using Horn
clauses; examples illustrating use of recursive Horn clauses;
preliminary discussion on solving Horn clauses |
| Oct 29 | Program verification through Horn clause solving: further examples; a naive way to solve Horn clauses as least fixed points of constraints, and its similarity to invariant computation in programs |
| Nov 3 | Discussion on various constraint solving techniques: conflict driven clause learning and backjumping in DPLL solvers, overview of DPLL(T) with examples, overview of a solver in the theory of uninterpreted functions with equality; summary of topics covered in entire course |
| Nov 5 | Guest lecture 1 by Ashutosh Gupta: generating proofs of unsatisfiability |
| Nov 6 | Guest lecture 2 by Ashutosh Gupta: generating interpolants from proofs |
|