CS615: Formal Specification and Verification of Programs
Autumn 2016


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Friendly Teaching Assistant Anand Babu email: anandb [AT] cse ...

Announcements

Course Description

The purpose of this course is to train students in the art and science of specifying correctness properties of programs and proving them correct. The primary emphasis will be on deductive and algorithmic verification techniques. There will be occasion to study some of the issues that arise in deploying these techniques in practice, and solution strategies for them. The course will make use of projects and tools to drive home different ideas taught in class.

Prerequisites

This is a graduate level course, and good working knowledge of propositional and first order logics, algorithm design and analysis are required for crediting/auditing this course. Some background in automata theory is also needed. These topics will not be reviewed in class, and the instructor will assume familiarity with them. Some topics in the theory of lattices are also required as pre-requisites. However, there will be an overview of these topics prior to their usage in lectures. If you are not sure whether you meet the prerequisites of this course, please meet the instructor at the earliest.
In propositional and first-order logic, you are expected to be familiar with the material in
  • Chapters 1 and 2 of Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan, Second Edition, Cambridge University Press
It would also help (although some of this will be quickly covered in the course) if you are familiar with the material in
  • Chapters 1 and 2 of Introduction to Lattices and Orders by B. A. Davey and H. A. Priestley, Second edition, Cambridge University Press,
A quick check for prerequisites: If you are comfortable answering all questions in this set , it is likely you meet the prerequisites for this course. However, if you are having problems answering these questions and still want to register for this course, please contact the instructor at the earliest.

Contact Hours

What When Where
Lectures Tue 15:30-16:55,
Fri 15:30-16:55
SIC 305, KReSIT Building
Office hour Wed 16:00-17:00 Room 314, New CSE Building
(by email appointment only)

Problem Sessions

When Where
Thurs, Sep 15, 6.00-7.30 pm SIC 305, KReSIT Building
Sat, Nov 11, 4.00-6.00 pm SIC 205, KReSIT Building

Related links ...

Grading (tentative schedule)

In-class quizes and tool-based projects 20%
Midterm 20%
Endterm 40%
Individual end-term project 20%

Project Policy

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

    Problems Graded? Expected to be completed by
    Key-Hoare exercises
    Please read this
    note on Key-Hoare first.
    Ungraded Aug 8, 2016
    In-class Key-Hoare based assignment
    Please check on moodle for problem statement
    Graded Aug 26, 2016
    Mid-sem exam Graded Sep 9, 2016
    Quiz 2 Graded Sep 23, 2016
    Quiz 3 Graded Oct 21, 2016

    Reading Material

    • Papers, chapters and articles to be announced in class.
    • Class notes.

    Current Reading List

    Propositional and predicate logic prerequisites
    1. 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
    1. Chapter 4 of Logic in Computer Science: Modeling and Reasoning about Systems by Michael Huth and Mark Ryan, Cambridge University Press
    2. A deck of slides used in Microsoft Research Summer School 2008. Skip the parts about Separation Logic for now.
    3. A short note on using Key-Hoare.
    Separation logic in program verification
    1. John Reynolds' seminal paper on Separation Logic is an excellent introduction to the topic.
    2. 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.
    3. A wonderful tutorial on Separation Logic given by Peter O'Hearn at CAV 2008.
    Abstract interpretation
    1. A wonderful tutorial by Prof. Cousot, explaining in fairly simple language what abstract interpretation is all about. Highly recommended for everybody taking this course.
    2. 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.
    3. Invited talk on "Proving Programs Correct by Abstract Interpretation" at WEPL 2015.
    4. Slides (in particular Lecture 15) of a course on Abstract Interpretation offered by Prof. Cousot at MIT in Spring 2005.
    5. 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.
    6. 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
    1. A beautiful introduction to the paradigm of Boolean Programs by Tom Ball and Sriram Rajamani
    2. 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.
    3. 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.
    4. 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