CSE-637: Program Semantics and Verification

Fall 2003

Class Place and Time:

CS 1223
Tue, Thu 3:50 -- 5:10pm

Prerequisites:

Graduate standing in the Computer Science Department; graduate courses in Logic (equivalent to CSE 541) and Programming Languages, or permission of instructor.

Topics:

This course will focus on issues in program analysis and verification, especially of concurrent programs.
In the class, we will initially cover semantics of programming languages, with focus on operational semantics. We will write programs encoding these operation semantics rules. We will then derive program analysis systems by modifying the semantics rules to capture abstract rather than concrete semantics.
While we build these systems, you will read papers on foundations of program analysis, and on a specific program analysis that we will decide later on. I am currently thinking of analyses for verifying information flow properties of programs, which are useful in describing security-relavent (privacy etc.) behaviors.
Based on this work in the first half of the semester, we will build a program analysis engine for inferring properties of nontrivial procedural programs (C/C++, Java source or Java class).

Schedule:

Class Date Day Topic Notes etc.

1 Sep 04 Th Organization and overview

2 Sep 09 Tu Operational Semantics of Imperative Programs opersem.old.tgz (Gzipped Tar Archive)

3 Sep 11 Th Operational Semantics of Programs with Procedures

4 Sep 16 Tu Operational Semantics of Programs with Procedures (contd.) opersem.tgz (Gzipped Tar Archive)

5 Sep 18 Th Denotations, Recursion and Least Fixed Points Slides (Gzipped Postscript),
Lambda Calculus Interpreter (Gzipped Tar Archive)

6 Sep 23 Tu Alternative Schemes for Operational Semantics

7 Sep 25 Th Abstract Semantics and Abstract Interpretation Abs. Interpreter (Gzipped Tar Archive)

8 Sep 30 Tu Data-Flow Analysis

9 Oct 2 Tu Program Analysis with Logic Programs -- 1

10 Oct 7 Th Semantics of Programs with Pointers Example programs (with parsers)

11 Oct 14 Th Analysis of Push-Down Systems (See papers on Interproccedural Dataflow Analysis via Graph Reachability by Thomas Reps, Susan Horowitz and Mooly Sagiv)

12 Oct 16 Tu Program Analysis with Logic Programs -- 3

13 Oct 21 Th Information Flow Analysis

14-28 Oct 23 -- Project progress (presentations & reports)

Oct 30 Th Information Flow Analysis & Points-To Analysis
Teams:
Points-To Analysis: Mahadev, Rahul, Dan, Nitesh, Sumit, Amit S.
Information Flow Analysis: Amit B., Alex, Liqiang, Giri, Dipti, Wei, Song Points-To Analysis survey
Empirical Comparison of Points-To Analyses
Fast Aliasing Analysis (this paper gives a nice deductive formulation of Andersen's points-to analysis)
Secure Information Flow

Class	Date	Day	Topic	Notes etc.
1	Sep 04	Th	Organization and overview
2	Sep 09	Tu	Operational Semantics of Imperative Programs	`opersem.old.tgz` (Gzipped Tar Archive)
3	Sep 11	Th	Operational Semantics of Programs with Procedures
4	Sep 16	Tu	Operational Semantics of Programs with Procedures (contd.)	`opersem.tgz` (Gzipped Tar Archive)
5	Sep 18	Th	Denotations, Recursion and Least Fixed Points	Slides (Gzipped Postscript), Lambda Calculus Interpreter (Gzipped Tar Archive)
6	Sep 23	Tu	Alternative Schemes for Operational Semantics
7	Sep 25	Th	Abstract Semantics and Abstract Interpretation	Abs. Interpreter (Gzipped Tar Archive)
8	Sep 30	Tu	Data-Flow Analysis
9	Oct 2	Tu	Program Analysis with Logic Programs -- 1
10	Oct 7	Th	Semantics of Programs with Pointers	Example programs (with parsers)
11	Oct 14	Th	Analysis of Push-Down Systems	(See papers on Interproccedural Dataflow Analysis via Graph Reachability by Thomas Reps, Susan Horowitz and Mooly Sagiv)
12	Oct 16	Tu	Program Analysis with Logic Programs -- 3
13	Oct 21	Th	Information Flow Analysis
14-28	Oct 23 --		Project progress (presentations & reports)
	Oct 30	Th	Information Flow Analysis & Points-To Analysis Teams: Points-To Analysis: Mahadev, Rahul, Dan, Nitesh, Sumit, Amit S. Information Flow Analysis: Amit B., Alex, Liqiang, Giri, Dipti, Wei, Song	Points-To Analysis survey Empirical Comparison of Points-To Analyses Fast Aliasing Analysis (this paper gives a nice deductive formulation of Andersen's points-to analysis) Secure Information Flow

Software:

Please see Wei Xu's code to convert C programs to ASTs in a Prolog format that you can use for subsequent analysis.

References:

For basic programming language semantics, the following books will be most useful:

Daniel Friedman, Mitchell Wand and Christopher Haynes, Essentials of Programming Languages.
MIT Press, 1992. ISBN 0-262-06145-7

John Mitchell, Foundations of Programming Languages.
MIT Press, 1996. ISBN 0-262-13321-0

Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction.
MIT Press, 1993. ISBN 0-262-23169-7

For FP systems, see SML, OCAML, Haskell, or the slightly dated comp.lang.functional FAQ.

Instructor:

C.R. Ramakrishnan
Office: 1420 Computer Science Building, 632-8218
Office Hours: Tue/Thu 9am-11am, or by appointment
email: cram AT cs DOT sunysb DOT edu

C.R. Ramakrishnan