CS615: Formal Specification and Verification of Programs
Spring 2014


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Friendly Teaching Assistant None yet  

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. 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 a quick overview of these topics prior to their usage in lectures.
CS719 or equivalent is a recommended pre-requisite for this course. If you have not taken CS719 or an equivalent course in the past, you are expected to complete background readings as specified below
  • By Jan 9, 2014 : 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
  • By Jan 27, 2014 : 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.

Hours

What When Where
Lectures Mon 15:30-17:00,
Thurs 15:30-17:20
SIC 205, KReSIT Building
Office hour Wed 17:00-18:00 CFDVS Lab 1 (Maths basement)
(by email appointment only)

Problem Sessions When Where
Session 1 Fri, Feb 21, 2-4.30 pm CFDVS

Related links ...

Grading

In-class quizes 20%
Midterm 20%
Endterm 40%
Individual 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). 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 exactly 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 according to a schedule to be announced later.

Some more logistics ...

  • Midterm and endterm exam, 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
    Quiz 1 Jan 20, 2014
    Quiz 2 Feb 17, 2014

    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.]
    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.
    Boolean programs and predicate abstraction
    1. A beautiful introduction to the paradigm of Boolean Programs by Tom Ball and Sriram Rajamani
    2. BLAST: Berkeley Lazy Abstraction Software Verification Tool web 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)
      • The Software Model Checker BLAST: Applications to Software Engineering by Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, Int. Journal on Software Tools for Technology Transfer, 2007.

    References for the more interested ...

    • An introductory talk on Hoare Logic given at Microsoft Research Summer School on Programming Languages, Analysis and Verification, 2008.

    Lecture Schedule

    Date Topics details
    Jan 6