THE
SCHEDULE IS VERY LIKELY TO CHANGE!
Date 
Topic 
Reading 
Lecture
Notes 
Homework 
Jan 16 
Introduction 


Jan 19 
Dataflow
Analysis:
The four classical dataflow problems 
Ch. 9.1 and 9.2 from the Dragon
Book 
HW1
(Dataflow) 

Jan 23 
DF: Lattices, transfer
functions, dataflow frameworks, MFP 
Ch. 9.2 and 9.3 from the Dragon
Book 


Jan 26 
DF: MOP vs. MFP.
Nondistributive analysis: constant propagation and pointsto analysis 
9.3 from the Dragon Book 

Jan 30 
Nondistributive analysis,
continued. 
HW1
due HW2 (Class analysis of Java with Soot) 

Feb 2 
Classical analysis for
objectoriented programs: CHA, RTA, XTA. Introduction to Soot 
Tip and Palsberg: ``Scalable Propagationbased
. . .``, OOPSLA`00 

Feb 6 
DF: Interprocedural
Analysis, ICFG, MORP, Context sensitivity 
Ch. 12.1 and 12.2 from the Dragon Book 

Feb 9 
DF: Interprocedural
Analysis, continued 

Feb 13 
IFDS and CFLreachability 
HW2
due, 

Feb 16 
Abstract
Interpretation: Semantics. Notion of abstraction 

Feb 23 
AI: Notion of abstraction,
continued 
HW3
due, 

Feb 27 
AI: Galois Connections, transformers 

Mar 2 
SNOW DAY 
HW4 due, HW5 (AI and
Haskell) 

Mar 6 
Types
and Typebased Analysis: Lambda calculus, reduction strategies, Haskell 
Ch. 5 and 6 from Pierce 
Quiz 4 

Mar 9 
Types: Simply typed lambda
calculus, type soundness theorem (progress and preservation) 
Ch. 8 and 9 from Pierce 

Mar 20 
Types: Simple type inference 
Ch. 22 and 23 from Pierce 
HW5 due 

Mar 23 
Types: Polymorphism, Hindley Milner type inference 
Ch. 22 and 23 from Pierce 
Quiz 5 

Mar 27 
Types: Hindley
Milner type inference, cont. Types for imperative languages 
Ch. 22 and 23 from Pierce 

Mar 30 
Types: Monads, Subtyping,
Pluggable types and applications: taint analysis for Android 

Apr 3 
Axiomatic Semantics: SMT solvers and applications. Hoare logic (more
formally than Principles!) 
HW6 due HW7 (Z3 and OCaml) 

Apr 6 
AS: Symbolic execution 
Quiz 6 

Apr 10 
NO CLASS 

Apr 13 

Apr 17 
HW7 due HW8 (Z3 and OCaml) 

Apr 20 

Apr 24 

Apr 27 

May 1 
HW8 due 