CS615: Formal Specification and Verification of Programs
Spring 2010


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Friendly Teaching Assistant Parakram Majumdar email: parakram [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 theoretical aspects of specification formalisms and on deductive and algorithmic verification. There will be occasion to study some of the issues that arise in deploying these techniques in practice, and solution strategies for them.

Prerequisites

This is a graduate level course, and good working knowledge of propositional and first order logics, algorithm design and analysis, and automata theory are required for crediting/auditing this course. CS719 or equivalent is a pre-requisite for this course.

Hours

What When Where
Lectures Tue 14:00-15:25,
Fri 14:00-15:20
SIC 201, KReSIT Building
Office hour Wed 17:00-18:00 CFDVS Lab 1 (Maths basement)
(by email appointment only)

Tutorials When Where
Coming soon ...

Related links ...

Grading

Quizzes + Homeworks 20%
Midterm 20%
Endterm 40%
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 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
    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. 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
    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. Slides (in particular Lecture 15) of a course on Abstract Interpretation offered by Prof. Cousot at MIT in Spring 2005.
    4. 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.