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


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

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


Jan 24 
DF: Dataflow frameworks, MOP
vs. MFP 
9.3 from the Dragon Book 
Quiz 1 

Jan 28 
DF: Nondistributive analysis:
constant propagation and pointsto analysis 
HW1
due HW2 (Class analysis of Java with Soot) 

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

Feb 4 
DF: Catchup 
Quiz 2 

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

Feb 11 
Interprocedural Analysis,
Context sensitivity in practice 
Ch. 12.1 and 12.2 from the Dragon Book 
HW2
due, 

Feb 14 
Abstract
Interpretation: Semantics. Notion of abstraction 
Ch. 12.2 from the Dragon Book 
Quiz 3 

Feb 19 
AI: Notion of abstraction,
continued 
HW4 (Optional) 

Feb 21 
AI: Galois Connections,
transformers 
HW3
due 

Feb 25 
AI: Galois Connections,
transformers, continued 
HW4 due, HW5 (AI and Haskell) 

Feb 28 
Types
and Typebased Analysis: Lambda calculus, reduction strategies, Haskell 
Ch. 5 and 6 from Pierce 

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

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

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


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

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

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

Apr 1 
AS: Symbolic execution 

Apr 4 
AS: Symbolic execution 

Apr 8 
Presentations, part 1 

Apr 11 
Presentations, part 2 
HW7 due HW8
(Z3 and OCaml) 

Apr 15 
Presentations, part 3 

Apr 18 
Presentations, part 4 

Apr 22 
Presentations, part 5 

Apr 25 
Presentations, part 6 
HW8 due 