CS615: Formal Specification and Verification of Programs
Autumn 2018


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Friendly Teaching Assistants Sparsa Roychowdhury email: sparsa [AT] cse ...

Announcements

  • Please subscribe to the moodle page for CS615 and to the piazza page for CS 615A at IIT Bombay. Note that the course number is CS615A on piazza. Please see posting on moodle to get the access code for enrolling in piazza.
  • Course marks and grades are available here. Happy vacations!

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,

Contact Hours

What When Where
Lectures Wed 09:30-11:00,
Fri 09:30-11:00 		SIC 301, KReSIT Building
Office hour Thurs 16:00-17:00 Room 314, New CSE Building
(by email appointment only)

Problem Sessions

When Where
TBA TBA

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 group (ideally of size 2) is required to do a small project as a hands-on exercise in building a formal verification tool. More details of projects will be submitted post mid-sem exam.

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 will be given close to end-sem exam. 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.

List of some formal verification tools relevant to the contents of this course.

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, see also this document from Chalmers University
    Please read this note on KeY-Hoare first.    		 Ungraded Jan 18, 2019
    Assignment 1 Graded Feb 13, 2019
    Quiz 1 Graded Feb 20, 2019
    Midsem Exam Graded Feb 27, 2019
    Quiz 2 Graded April 17, 2019
    Endsem Exam Graded April 27, 2019

    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.
    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. Introductory slides on "Proving Programs Correct by Abstract Interpretation" .
    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. 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)
    5. A wonderful set of slides on the BLAST model checker, by Tom Henzinger, Ranjit Jhala and Rupak Majumdar. [I'm mirroring the slides here because I can no longer find a link to the original slides.]
    Combining abstract interpretaters
    1. A nice set of slides by Prof. Agostino Cortesi on product operators to combine abstract domains
    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
    Jan 4 Introduction and motivation for formal specification and verification; notion of program state (stack x heap); programs as state transition systems
    Jan 8 Introduction to Hoare logic; a simple imperative language and a simple assertion language, notion of weakest pre-condition, Hoare inference rules for assignment, sequential composition, conditional branches, pre-condition weakening and post-condition strengthening.
    Jan 11 More on Hoare inference rules: while loops, loop invariants, notion of inductive invariants. Soundness and relative completeness of Hoare proof system. Discussion on strongest post-condition and its relation to weakest pre-condition. Brief demo of KeY-Hoare tool being used to prove properties of a simple program using Hoare logic.