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: Galois Connections 
HW3
due, HW4 

Feb 27 
Types
and Typebased Analysis 

Mar 2 
Types: Simply typed lambda
calculus 
HW4 due, HW5 (AI, Types and Haskell) 

Mar 6 
Types: Formal account:
semantics and type soundness 

Mar 9 
Types: HindleyMilner
type Inference. Polymorphism (parametric) 
HW5 due HW6 

Mar 20 
Presentations, part 1 

Mar 23 
Presentations, part 2 


Mar 27 
Subtyping 

Mar 30 
Types: Types for imperative
programs 
HW6 due HW7 (Pluggable types with Checkers or Soot) 

Apr 3 
Types: Pluggable types, JSR308,
with Checkers and Soot 

Apr 6 
Types: Pluggable types, applications:
information flow for Android 

Apr 10 
Axiomatic Semantics: Hoare logic (more formally than Principles!) 
HW7 due HW8 

Apr 13 
AS: SMT solvers and applications 

Apr 17 
Symbolic execution 

Apr 20 
Presentations, part 3 
HW8 due, HW9 (Verifier with Z3) 

Apr 24 
Presentations, part 4 

Apr 27 
Presentations, part 5 

May 1 
Presentations, part 6 
HW9 due 