CIS 905, Spring 2005

Instructors:

Torben Amtoft and Anindya Banerjee.

Time:

Tuesdays, noon-2:30pm in N236.

Form of class:

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

Material

• Nielson & Nielson & Hankin: Principles of Program Analysis (NNH).

Log

January 25

Anindya introduces the basics of abstract interpretation, using slides from part I of Dave Schmidt's Uruguay lectures (pp 3-22) and own slides (pp 1-7) and slides from NNH (pp 1-2,5-7,9-12,14-20).
For next time, please read (in NNH) the proof of Lemma 4.5 and also that of Proposition A.10.

February 1

Anindya continues abstract interpretation, with focus on Galois Connections, using slides from NNH (pp 37-55) and proving key properties on the board.

In order to clarify some confusion about how the concretization function works on "junk" abstract elements, David Schmidt talked briefly about how to generate Galois connections from binary relations, as described in Section 3 of his recent paper (where Section 5 connects simulations and Galois connections, by means of powerset domains and logical relations.)

February 8

Anindya continues abstract interpretation, using slides from part II of Dave Schmidt's Uruguay lectures (pp 15-26) and proving key properties on the board, also using own slides on application in information flow analysis.

February 15

Anindya briefly talkes about closure maps, using slides from part II of Dave Schmidt's Uruguay lectures (pp 12-13).
Edwin Rodriguez presents the notions of widening and narrowing, using slides from NNH (pp 17-36).

February 22

We cover part III of Dave Schmidt's Uruguay lectures, with Scott Harmon taking the first part (pp 1-22) and Anindya taking the last part (pp 27-38).

March 1

Sruthi Bandhakavi

1. covers the shape analysis (based on work by Sagiv & Reps & Wilhelm) of Section 2.6 in NNH, using pp 110-151 of the slides from NNH (see here for the result of analyzing the list reversal program using a somewhat more precise variant which takes tests into account);
2. starts on the paper Parametric shape analysis via 3-valued logic (also by Sagiv & Reps & Wilhelm).

March 8

No class, instead we'll have a joint session with our visitor Alex Aiken.

March 10 (noon-2:30pm, in conference room.)

1. Sruthi finishes Parametric shape analysis via 3-valued logic.
2. Torben starts presenting the pi-calculus, using material from Daniel Hirschkoff's course on mobility. Today, we covered the introductory slides.

March 15

No class, as instructors out of town.

March 17 (noon-2:30pm, in conference room.)

Dave Schmidt presents part IV of his Uruguay lectures, on applications and logics for static analysis.

March 29

Torben continues the pi-calculus, using material from Daniel Hirschkoff's course on mobility: after we have formalized the syntax and semantics of the calculus, we discuss how to assign types to processes.

April 5

No class, as instructors are out of town.

April 12

Torben almost finishes the pi-calculus, using material from Daniel Hirschkoff's course on mobility, motivating and discussing behavioral equivalences (slides 1-95).

April 19

Motivated by the visit by John Reynolds, Edwin presents separation logic: after some introductory slides, we look at applications to concurrent programming.

April 26 (in library)

Isabella Mastroeni presents her doctoral thesis work, published in POPL'04 and in CSL'04 and in ESOP'05.

May 3 (last day of semester)

1. Scott gives introduction to type and effect systems. using slides from NNH.
2. Sruthi present work in progress on information flow analysis for heap languages.