CS402: Selected Case Studies in Computer Systems: Formal Verification of Programs
Autumn 2012


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Friendly Teaching Assistant Sukanya Basu email: sukanyab [AT] cse ...

Announcements

Course Description

The purpose of this course is to train students in the art and science of formally proving properties of sequential programs. The primary emphasis will be on algorithmic verification techniques that lend themselves to automation. 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 an advanced undergraduate/introductory 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.
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 Tue 15:30-16:55,
Fri 15:30-16:50
SIC 205, KReSIT Building
Office hour Mon 17:00-18:00 CFDVS Lab 1 (Maths basement)
(by email appointment only)

Related links ...

Grading

Quiz 20%
Midterm 20%
Endterm 40%
Project 20%

Project Policy

Each student is required to do a medium-scale project as a hands-on exercise in formal verification of programs 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 individually (no groups). 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.

Useful links for your projects:

  • BLAST code/executable/documentation
  • Some "open source software" sources:
    • Cross-referenced source for Linux and some other open source software
    • Google Code . Click on a project label, choose a software and then click on the "Source" tab to find instructions to checkout source code.
    • Sourceforge.net : A large open source software repository.
    • Freshmeat.net : An index of Unix and cross-platform software, lots of them under "open source" license. You should only use software that has the "free for educational use" license.

Some more logistics ...

  • Midterm and endterm exam, and quizes 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. However, copying solutions from others will be severely penalized. To understand the distinction between "copying" and "discussion", please read this.
  • 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' CS615 home pages [2010, 2008, 2007, 2006, 2005, 2004]
Midsem Exam Sep 15, 2012
Take home quiz 1 Due by Sat, Nov 24, 2012
Take home quiz 2 Due by Sat, Nov 24, 2012
Take home quiz 3 Due by Sat, Nov 24, 2012
Endsem Exam Nov 24, 2012

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
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 (but the PDF/PS slides seem unavailable at the moment).
  2. Abstract Interpretation in a Nutshell by Prof. Cousot -- also a must-read to understand the basics of abstract interpretation.
  3. 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.
  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. Refinement in abstract domains like octagons and polyhedra
    • 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
    • Automatically Refining Abstract Interpretations by Bhargav S. Gulavani, Supratik Chakraborty, Aditya Nori and Sriram K. Rajamani, in Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2008. A journal version containing some proofs omitted in the above paper appears here .
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.
Shape analysis (reasoning about heaps)

References for the more interested ...

  • An introductory talk on Hoare Logic given at Microsoft Research Summer School on Programming Languages, Analysis and Verification, 2008.
  • The Key Project for verifying Java/JavaCard programs -- a good tool to try out Hoare logic in action.
  • Prof. Cousot's course on Abstract Interpretation at MIT in Spring 2005.
  • Some slides (rather incomplete) used in class lectures on regular model checking. Please also read sections 7.1 through 7.5 of the more detailed reference material on this topic.