Computer Science 357D Static Analysis of Programs and Reactive Systems  Spring 2007

Lectures: Tuesdays and Thursdays 1:15 - 2:30 pm in Gates 498
Instructors: Dr. Henny Sipma and Prof. Zohar Manna

Table of Contents

Class Schedule

Lecture	Date	Topic	Lecture Notes	References
1	April 3	Course overview	slides
2	April 5	Transition systems and property satisfaction	slides	[MP95]
3	April 10	Proving invariants	slides
4	April 12	Preconditions and backward propagation	slides
5	April 17	Postconditions and forward propagation
6	April 19	Karr's analysis		[Karr76]
7	April 24	Abstract interpretation -- Introduction	slides
8	April 26	Orders and Lattices	slides	[DP02]
9	May 1	Abstract interpretation -- Theory
10	May 3	Abstract interpretation -- Polyhedral analysis
11	May 8	Abstract interpretation -- Analysis in other numerical domains
12	May 10	Abstract interpreation -- Template Constraint Matrices		[SSM05]
13	May 15	Abstract interpretation -- Template Constraint Matrices
14	May 17	Constraint-based Analysis -- Invariant generation		[CSS03],[SSM04]
15	May 22	Constraint-based Analysis -- Generation of ranking functions		[BMS05]
16	May 24	Predicate abstraction
17	May 29	Shape Analysis		[SRW98]
18	June 1	Shape Analysis

References:

• [MP95] Zohar Manna and Amir Pnueli, Temporal Verification of Reactive Systems: Safety. Springer Verlag, 1995.
  (Lectures 2, 3)

• [Karr76] Michael Karr, Affine Relationships Among Variables of a Program, Acta Informatica 6, pp 133-151, 1976.
  (Lecture 6)

• [DP02] B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press, 2nd ed, 2002.
  (Lecture 8)

• [SSM05] Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Scalable Analysis of Linear Systems using Mathematical Programming, In Proc.of Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, pp 21-47, Springer Verlag, 2005.
  (Lectures 12, 13)

• [CSS03] Michael A. Colon, Sriram Sankaranarayanan, Henny B. Sipma. Linear Invariant Generation using Non-linear Constraint Solving. In Computer Aided Verification (CAV 2003), vol. 2725 of Lecture Notes in Computer Science, Springer Verlag, pp. 420-433, 2003.
  (Lecture 14)

• [SSM04] Sriram Sankaranarayanan, Henny Sipma, Zohar Manna, Petri Net Analysis Using Invariant Generation. In Verification: Theory and Practice, vol. 2772 of Lecture Notes in Computer Science, 2003.
  (Lecture 14)

• [BMS05] Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Linear Ranking with Reachability, In Proc. of 17th International Conference on Computer Aided Verification (CAV'05), Springer Verlag, 2005, LNCS 3576, pp 491-504.
  (Lecture 15)

• [SRW98] Sagiv, M., Reps, T., and Wilhelm, R., Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems 20, 1 (January 1998), pp. 1-50.
  (Lectures 17, 18)

General Course Information

Instructor:

Henny B. Sipma and Zohar Manna
Computer Science Department
sipma at cs.stanford.edu ; manna at cs.stanford.edu

Description: (top)

This course presents fundamental principles and techniques to support static analysis for sequential and concurrent programs and reactive systems. Static analysis methods aim to discover properties of a system from the system description, rather than from simulations.

The course is divided in three parts. In the first part we present two principal techniques of program analysis: symbolic simulation based on abstract interpretation and constraint-based methods. Abstract domains considered include linear equalities, linear inequalities, and boolean algebras. In this part our model of computation will be the first-order model based on state transition systems.

The second part is devoted to decision procedures and their combination. Decision procedures are algorithms that can decide the validity of formulas in decidable theories. When applied in program analysis they can increase precision of the analysis considerably by eliminating infeasible paths. Theories we will consider include sets, recursive data structures, and queues, and their combination with Presburger arithmetic.

In the third part we will move to a model of computation that is closer to that of modern program languages, with support for dynamic memory allocation. To reason about these models we study shape analysis and separation logic.

Units: 3

Grading:

• Pass/no credit: based on attendance
• Letter grade: project

Final Project:

Options:

• 1-hour lecture: Select a topic relevant to the class and present a 1-hour lecture in class to explain the topic.
• Survey paper: Read five or more papers on a particular topic related to static analysis and write a 5-10 page survey and critique of these papers. (Some suggestions for topics).
• Research paper: Select a topic related to static analysis and develop something new. This can be an extension or specialization of an existing method to a particular class of programs, a new abstract domain, a new computational model for a particular class of programs, a new heuristic, etc.
• Implementation: Implement a static analysis method. This can be a stand-alone implementation, or it can be implemented on top of an existing platform, such as piVC (used in CS156, implemented in OCaml), or STeP (Stanford Temporal Prover, implemented in Java), which provide expression packages and parsers. Another option is to add a method to an existing static analysis tool such as FindBugs (for Java) or Saturn (for C).
• Implementation: Implement an existing decision procedure and experiment with your implementation on benchmarks (available at SMT-LIB (Satisfiability Modulo Theories Library).

Handouts:

We will be handing out notes on the topics covered and slides will be available on this website.

Text Book:

There is no required text book. The following two books may be useful for reference:

• Zohar Manna and Amir Pnueli, Temporal Verification of Reactive Systems. Safety, Springer 1995.
  We will be using the basic computational model presented in this book (Chapter 0), and rules for proving invariants (Chapter 1). However, these will also be covered by Notes.
• Flemming Nielson, Hanne R. Nielson, Chris Hankin, Principles of Program Analysis, Springer 1999.
  This book covers program analysis and abstract interpretation, but from a somewhat different perspective.
• B.A. Davey, H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press, 2nd ed, 2002.
  Orders are the basis of abstract interpretation.

---

Questions? Contact: sipma@cs.stanford.edu