CIS 905, Spring 2003

Theory of Programming Languages

Program Analysis

Program analysis enables one to predict, prior to run-time, a safe approximation of the values or behaviors arising during run-time when executing a program on a computer. For many years, the technology has been used in compilers so as to optimize the code generated, for example by not computing results that turn out not to be needed. Among the more recent applications is the validation of software (possibly downloaded from the Internet), thus reducing the likelihood of malicious or unintended behavior.

In order to rely on the results of program analysis, a firm mathematical foundation is necessary. In this course we shall give an overview of the main approaches to program analysis and cover the basic principles, with emphasis on type and effect systems and abstract interpretation.

Further information

Textbook

Nielson & Nielson & Hankin: Principles of Program Analysis.
A number of on-line tools are available from the web site; we briefly looked at the PAG/WWW system.
Along the way, we update an additional errata list.

Topics covered:

Chapter 1: Introduction, overview
Sections 2.1-2.5: Data Flow Analysis (brief summary only)
Section 2.6: Shape analysis
Chapter 4: Abstract Interpretation
Oksana Tkachuk & Matthew Dwyer: Adapting Side Effects Analysis for Modular Program Model Checking. (To appear in ESEC/FSE 2003.)
Presentation.
Thomas Ball and Andreas Podelski and Sriram K. Rajamani: Boolean and Cartesian Abstraction for Model Checking C Programs. (TACAS'2001, LNCS 2031.)
Torben Amtoft: Minimal Thunkification. (WSA'1993, LNCS 724.)
Presentation.
David Schmidt: Binary Relations for Abstraction and Refinement. (CIS Technical Report 2000-3. Corrected version of a paper in Proc. Workshop on Refinement and Abstraction, Amagasaaki, Japan, Nov. 1999. To appear in Elsevier Electronic Notes in Theoretical Computer Science.)
Presentation.
Patrick & Radhia Cousot: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. (Invited paper for PLILP'92, LNCS 631.)
Patrick & Radhia Cousot: Inductive definitions, semantics and abstract interpretation. (POPL'92.)
David Monniaux: Abstract interpretation of probabilistic semantics (SAS'00) and An abstract analysis of the probabilistic termination of programs (SAS'01).
Torben Amtoft and Franklyn Turbak: Faithful Translations between Polyvariant Flows and Polymorphic Types. (ESOP 2000, LNCS 1782.)
Presentation.

See this log file for what was covered when (and for homework assignments).

Instructor:

Torben Amtoft.

Time:

Tuesday and Thursday, 10:00am-11:30am in N127.

Form of class:

Lectures. Student presentations are encouraged, in particular later in the course. Larger projects could arise from this class.

Credit:

Handing in homework and/or giving presentations (and of course, attending regularly).

Prerequisites:

Some amount of "mathematical maturity", in particular within discrete mathematics;
CIS 505;
preferably also CIS 705 (or CIS 706).

Torben Amtoft