Captain's Log: Theory of Programming Languages (CIS 905), Spring 2003
Introduced ourselves; agreed to meet Tue and Thu from 10:00am to 11:15am.
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
to be solved iteratively.
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.
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.
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
Homework for Tue Feb 4: Exercise 1.3.
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).
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.
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).
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
presenting the transfer function for x := a.
Completed Section 2.6.3, giving transfer functions for
x := y,
x.sel := a,
x.sel := y,
(In all cases, x != y.)
Finished Shape Analysis by
working out Exercise 2.21 on the board,
at the same time resolving some subtle issues.
her work on alias and side-effect analysis.
William Deng gave a short tutorial on the
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.
Started on Section 4.3, motivating (as on pp.239-240)
the concept of Galois connections.
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.
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.
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.
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.
Correctness and Optimality of Induced Analysis (p.258).
Motivate the concept of Widening (Figures 4.3 and 4.4).
Widening (Section 4.2.1), also looking at Exercises 4.6 and 4.8.
Homework for Thu Apr 3: Exercise 4.9.
Induced widening (Section 4.5.3).
Narrowing (Section 4.2.2).
Homework for Tue Apr 8: Exercise 4.23.
William Deng presented
Boolean and Cartesian Abstraction for Model Checking
(also appears in proceedings of TACAS'2001, LNCS 2031).
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
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).
Minimal Thunkification by Torben Amtoft.
(Proceedings of WSA 1993, Springer LNCS 724 pp.218-229.)
Looked at Mini Project 4.1.
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.)
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.)
Present most of Comparing the Galois connection and widening/narrowing approaches to abstract interpretation by Patrick & Radhia Cousot
(Invited paper for PLILP'92).
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.)
Finish Inductive definitions, semantics and abstract interpretation by
covering some of the example applications.
Abstract interpretation of probabilistic semantics
An abstract analysis of the probabilistic termination of programs
Abstract interpretation of probabilistic semantics
An abstract analysis of the probabilistic termination of programs.
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.)
Oksana Tkachuk presents her ongoing work on proving the correctness of
and side-effect analysis.
slides 9--13 of Faithful Translations between Polyvariant Flows and Polymorphic Types.
Have a good summer! :)