Captain's Log: Theory of Programming Languages (CIS 905), Spring 2003

January 16

Introduced ourselves; agreed to meet Tue and Thu from 10:00am to 11:15am.

January 21

General principles (Sect. 1.1) such as safe approximations and undecidability. Example analysis: reaching assignments (Sect 1.2). One way to compute that analysis is by means of data flow equations (Sect. 1.3.1) to be solved iteratively.

January 23

A monotone functional on a finite lattice has a computable least fixed point, and hence data flow equations as in Sect. 1.3.1 have a least solution which can be computed easily by hand using chaotic iteration (Sect. 1.7). A collecting semantics for our example program was presented; it is well-defined since any monotone functional on a (not necessily finite) complete lattice has a least fixed point (Proposition A.10).
Homework for Tue Jan 28: Exercise 1.8.

January 28

Considered a transformation using reaching assignments (Sect. 1.8); note that after each step the original analysis is still valid and optimal but if the rules suggested by Exercise 1.10 are included then the original analysis does not necessarily remain optimal (though still valid). Motivated the notion of Galois connections for relating a concrete domain to an abstract domain (Sect. 1.5).
Homework for Thu Jan 30: Exercises 1.9, 1.11.

January 30

Induced analysis (from collecting trace semantics) for reaching assignments (Sect. 1.5). A couple of type systems for reaching assignments (Sect. 1.6.1), where one involves subtyping which might be "inlined". Discussed to which degree all analysis frameworks are equivalent (cf. Preface).
Homework for Tue Feb 4: Exercise 1.3.

February 4

Discussed Exercises 1.8, 1.9, 1.11. Finished discussion of the annotated type systems in Table 1.3. Brief introduction to the lambda-calculus. An effect system for call-tracking analysis (Sect. 1.6.2).

February 6

Solved Exercise 1.3. Covered Control flow analysis (Sect. 1.4).
Discussed which direction to take next. A consensus emerged that we should look into Abstract Interpretation, after having introduced Shape Analysis.
Homework for Tue Feb 11: Exercise 1.2.

February 11

Briefly summarized Sections 2.1-2.5: classifying analyses wrt. whether they are forwards or backwards and wrt. whether they are "may" or "must"; the Meet Over all Paths (MOP) approach (more precise for a non-distributive framework like constant propagation but potentially undecidable); interprocedural analysis (where each procedure may be called from several places).
Embarked on Shape Analysis, presenting the pointer language and its semantics (Section 2.6.1).

February 13

Defined the notion of a shape graph so as to abstract the structure of the heap (Section 2.6.2). Then embarked on developing a (forward and "may") shape analysis (Section 2.6.3), presenting the transfer function for x := a.

February 18

Completed Section 2.6.3, giving transfer functions for the statements malloc(x), x := y, x.sel := a, x.sel := y, x:= y.sel. (In all cases, x != y.)

February 20

Finished Shape Analysis by working out Exercise 2.21 on the board, at the same time resolving some subtle issues.

February 25

Oksana Tkachuk presented her work on alias and side-effect analysis.

February 27

William Deng gave a short tutorial on the PAG system.
We specified the correctness of certain kind of analyses by means of correctness relations and representation functions (Section 4.1, except for 4.1.3).
Homework for Tue Mar 4: Exercise 4.1.

March 4

Started on Section 4.3, motivating (as on pp.239-240) the concept of Galois connections.

March 6

Continued Section 4.3 on Galois connections, with focus on the Interval lattice (Example 4.19). Proved the equivalence of various definitions (Lemmas 4.22 and 4.23).
Homework for Tue Mar 11: Exercise 4.13.

March 11

Continued the theory of Galois connections (Section 4.3). Special case: a Galois insertion (Section 4.3.2). Construction of Galois connection from representation function, and from extraction function (p.235). Combining Galois connections (Section 4.4): sequential composition (p.245), total function space (p.250).
Homework for Thu Mar 13: Exercise 4.15.

March 13

Continued on combining Galois connections (Section 4.4): independent attribute method vs. relational method, direct product vs. direct tensor product.
Homework for Tue Mar 25: Exercise 4.21.

March 17--21

Spring break

March 25

Galois connections between Monotone function spaces (p. 251) and Inducing along the abstraction function (Section 4.5.1). Approximation of fixed points (Lemma 4.42). Correctness expressed using logical relations (Section 4.1.3). Application to Data Flow Analysis (Section 4.5.2) where we gave what the authors call "direct" or "concrete" proofs of the results.
Homework for Thu Mar 27: Exercise 4.5.

March 27

Correctness and Optimality of Induced Analysis (p.258). Motivate the concept of Widening (Figures 4.3 and 4.4).

April 1

Widening (Section 4.2.1), also looking at Exercises 4.6 and 4.8.
Homework for Thu Apr 3: Exercise 4.9.

April 3

Induced widening (Section 4.5.3). Narrowing (Section 4.2.2).
Homework for Tue Apr 8: Exercise 4.23.

April 8

William Deng presented Boolean and Cartesian Abstraction for Model Checking C Programs (also appears in proceedings of TACAS'2001, LNCS 2031).

April 10

Wrapped up Chapter 4 by going through Exercises 4.9, 4.23, and briefly also Exercises 4.24 and 4.11. Elaborated on the correctness of the trivector transformation presented April 8. Discussed some ideas for how to spend the rest of the course.
Homework for Tue Apr 15: Mini project 4.1 (Galois connection for lists).

April 15

Present Minimal Thunkification by Torben Amtoft. (Proceedings of WSA 1993, Springer LNCS 724 pp.218-229.)

April 17

Looked at Mini Project 4.1.
Present the first 14 slides of Binary Relations for Abstraction and Refinement by David Schmidt. (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.)

April 22

Present the rest of Binary Relations for Abstraction and Refinement.
Give basic motivation for Types as Abstract Interpretations by Patrick Cousot. (Invited paper for POPL'97, Paris, ACM Press.)

April 24

Present most of Comparing the Galois connection and widening/narrowing approaches to abstract interpretation by Patrick & Radhia Cousot (Invited paper for PLILP'92).

April 29

Finish Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, covering some of the widenings mentioned there.
Present the main idea of Inductive definitions, semantics and abstract interpretation by Patrick & Radhia Cousot. (POPL'92.)

May 1

Finish Inductive definitions, semantics and abstract interpretation by covering some of the example applications.
Start presenting Abstract interpretation of probabilistic semantics (SAS'00) and An abstract analysis of the probabilistic termination of programs (SAS'01) by David Monniaux.

May 6

Finish Abstract interpretation of probabilistic semantics and An abstract analysis of the probabilistic termination of programs.
Present slides 1--8 of Faithful Translations between Polyvariant Flows and Polymorphic Types by Torben Amtoft and Franklyn Turbak. (Proceedings of ESOP 2000, Springer LNCS 1782 pp.26-40.)

May 8

Oksana Tkachuk presents her ongoing work on proving the correctness of alias and side-effect analysis.
Present slides 9--13 of Faithful Translations between Polyvariant Flows and Polymorphic Types.
Have a good summer! :)