Lecture Notes


Jan 10



Lecture1 [ppt, pdf]


Jan 14

Dataflow (DF) Analysis: The four classical dataflow problems

Ch. 9.1 and 9.2 from the Dragon Book

Lecture2 [ppt, pdf]

HW1 (Dataflow)

Jan 17

DF: Lattices, transfer functions, dataflow frameworks, MFP

Ch. 9.2 and 9.3 from the Dragon Book

Lecture3 [ppt, pdf]


Jan 24

DF: Dataflow frameworks, MOP vs. MFP

9.3 from the Dragon Book

Quiz 1


Lecture4 [ppt, pdf]

Jan 28

DF: Non-distributive analysis: constant propagation and points-to analysis

Lecture5 [ppt, pdf]

HW1 due

HW2 (Class analysis of Java with Soot)

Jan 31

Classical analysis for object-oriented programs: CHA, RTA, XTA. Introduction to Soot

Tip and Palsberg: ``Scalable Propagation-based . . .``, OOPSLA`00

Lecture6 [ppt, pdf]

Feb 4

DF: Catch-up

Lecture7 [ppt, pdf]


Quiz 2

Feb 7

DF: Interprocedural Analysis, ICFG, MORP, Context sensitivity

Ch. 12.1 and 12.2 from the Dragon Book

Lecture8 [ppt, pdf]

Feb 11

Interprocedural Analysis, Context sensitivity in practice

Ch. 12.1 and 12.2 from the Dragon Book

Lecture9 [ppt, pdf]

HW2 due,


Feb 14

Abstract Interpretation: Semantics. Notion of abstraction

Ch. 12.2 from the Dragon Book

IFDS slides [ppt, pdf]

Lecture10 [ppt, pdf]


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 Type-based 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


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