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 welldefined 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 lambdacalculus.
An effect system for calltracking 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.12.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 nondistributive 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 sideeffect 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.239240)
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 1721

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.218229.)

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 20003. 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 18 of Faithful Translations between Polyvariant Flows and Polymorphic Types by Torben Amtoft and Franklyn Turbak. (Proceedings of ESOP 2000, Springer LNCS 1782 pp.2640.)

May 8

Oksana Tkachuk presents her ongoing work on proving the correctness of
alias
and sideeffect analysis.
Present
slides 913 of Faithful Translations between Polyvariant Flows and Polymorphic Types.
Have a good summer! :)
Torben Amtoft