THE SCHEDULE IS VERY LIKELY TO CHANGE!

 

Date

Topic

Reading

Lecture Notes

Homework

Jan 16

Introduction

Syllabus

Lecture1 [ppt, pdf]

 

Jan 19

Dataflow Analysis: The four classical dataflow problems

Ch. 9.1 and 9.2 from the Dragon Book

Lecture2 [ppt, pdf]

HW1 (Dataflow)

Jan 23

DF: Lattices, transfer functions, dataflow frameworks, MFP

Ch. 9.2 and 9.3 from the Dragon Book

Lecture3 [ppt, pdf]

 

Jan 26

DF: MOP vs. MFP. Non-distributive analysis: constant propagation and points-to analysis

9.3 from the Dragon Book

Lecture4 [ppt, pdf]

Jan 30

Non-distributive analysis, continued.

Lecture5 [ppt, pdf]

HW1 due

HW2 (Class analysis of Java with Soot)

Feb 2

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

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

Lecture6 [ppt, pdf]

Feb 6

DF: Interprocedural Analysis, ICFG, MORP, Context sensitivity

Ch. 12.1 and 12.2 from the Dragon Book

Lecture7 [ppt, pdf]

Feb 9

DF: Interprocedural Analysis, continued

Lecture8 [ppt, pdf]

Feb 13

IFDS and CFL-reachability

Lecture9 [ppt, pdf]

HW2 due,

HW3

Feb 16

Abstract Interpretation: Semantics. Notion of abstraction

Lecture10 [ppt, pdf]

Feb 23

AI: Galois Connections

HW3 due,

HW4

Feb 27

Types and Type-based 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: Hindley-Milner 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