Textbooks & primary references

NNH
Nielson, Nielson, Hankin. Principles of Program Analysis. Springer, 2005.
M&S
Møller & Schwartzbach. Static Program Analysis. cs.au.dk/~amoeller/spa/ (free).
Aho
Aho, Lam, Sethi, Ullman. Compilers: Principles, Techniques & Tools, 2nd ed.
FB
Zeller, Gopinath, Böhme, Fraser, Holler. The Fuzzing Book. fuzzingbook.org.
Week 1 · Topic 1 — FoundationsJul 27 – 29
Readings for this week will be posted when the week begins.

L1. Course intro & motivation

Mon 27 Jul 2026 (Mon-1) · Topic 1
Slides
L1 — Course intro & motivation (PDF)
Handout
L1 — handout (PDF)
Follow
Paper
Outline
Why analyze programs; kinds of bugs and vulnerabilities; a tour of the course; grading, logistics, tools.

L2. Static, dynamic, and hybrid analysis; program invariants

Tue 28 Jul (Tue-1) · Topic 1
Handout
L2 — handout (PDF)
Follow
NNH §1.1–1.3; RY ch. 1
Paper
Ernst, “Static and Dynamic Analysis: Synergy and Duality”, WODA 2003; Ernst, Cockrell, Griswold, Notkin, “Dynamically Discovering Likely Program Invariants…” (Daikon), TSE 2001.
Outline
Static vs dynamic vs hybrid; running examples; what an “invariant” is; over- and under-approximation.

L3. Vulnerability assessment and secure coding

Wed 29 Jul (Wed-1) · Topic 1
Slides
L3 — Vulnerability assessment and secure coding (PDF)
Handout
L3 — handout (PDF)
Follow
Paper
Wagner, Foster, Brewer, Aiken. “A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities”, NDSS 2000; One. “Smashing the Stack for Fun and Profit”, Phrack 1996.
Outline
Threat models; common vulnerability classes (memory safety, integer overflow, injection)
Week 2 · Topic 1 — Foundations (metrics & IRs)Aug 3 – 5
Readings for this week will be posted when the week begins.

L4. Soundness, completeness, undecidability

Mon 3 Aug (Mon-2) · Topic 1
Slides
L4 — Soundness, completeness, undecidability (PDF)
Handout
L4 — handout (PDF)
Outline
Rice's theorem; sound vs complete analyses; soundy analyses in practice.

L5. Precision, recall, F-measure for analyzers

Tue 4 Aug (Tue-2) · Topic 1
Slides
L5 — Precision, recall, F-measure for analyzers (PDF)
Handout
L5 — handout (PDF)
Outline
True/false positives & negatives

L6. Program representation: AST, CFG, intermediate representations

Wed 5 Aug (Wed-2) · Topic 1
Slides
L6 — Program representation (PDF)
Follow
Aho ch. 5 & 8; NNH §1.5; Introduction to the Clang AST; CIS 547 — LLVM Framework Primer
Paper
Cytron et al. 1991 (SSA).
Outline
What LLVM is and how its front-end/back-end pipeline fits together; abstract syntax trees; the Clang AST (inspect / detect / transform); dumping a tree with clang++ -Xclang -ast-dump -fsyntax-only; reading an AST dump; branch instrumentation as a worked example; from AST to CFG to IR.
Week 3 · Topic 1 — LLVM & Clang toolingAug 10 – 12
Readings for this week will be posted when the week begins.

L7. Clang tutorial: libtooling & AST-based analysis

Mon 10 Aug (Mon-3) · Topic 1
Slides
L7 — Clang tutorial (external PDF, KAIST CS492)
Follow
LibTooling; RecursiveASTVisitor-based ASTFrontendActions; AST Matchers tutorial
Outline
Building a stand-alone Clang tool; ASTFrontendAction and ASTConsumer; walking the tree with RecursiveASTVisitor; SourceManager and source locations; rewriting source with Rewriter; coverage instrumentation at the source level.
Note
Delivered from the KAIST CS492 Clang tutorial deck linked above; the AST material it builds on is in L6.

L8. LLVM IR

Tue 11 Aug (Tue-3) · Topic 1
Slides
L8 — LLVM IR (PDF)
Follow
LLVM Language Reference; CIS 547 — LLVM Framework Primer; Lattner & Adve 2004
Paper
Lattner & Adve 2004 (LLVM design).
Outline
The LLVM pipeline: Clang front end → IR → opt passes → back end; analysis vs transformation passes; the three IR formats (in-memory, bitcode .bc, textual .ll); clang -S -emit-llvm; module / function / basic block / instruction structure; iterating the IR (STL, auto, inst_iterator); introduction to SSA form and why it helps analysis.

L9. LLVM IR (continued): CFGs & the LLVM class hierarchy

Wed 12 Aug (Wed-3) · Topic 1
Slides
L9 — LLVM IR continued (PDF)
Follow
LLVM Programmer's Manual; llvm::Value / llvm::Instruction doxygen
Outline
C program → LLVM IR walk-through; basic blocks and the CFG (opt -p=dot-cfg); SSA — one definition per variable, instruction as value name; printing with outs()/errs(); the class hierarchy Value → User → Instruction; isa/cast/dyn_cast; LoadInst, StoreInst, BinaryOperator, PHINode; BasicBlock and Function traversal.
Announced
From Week 4 onwards the class meets on Tuesday, Wednesday and Thursday. HW-1 released (due Fri 21 Aug, 23:59 IST).
Week 4 · Topic 1 — Specifications, Hoare logic & invariantsAug 18 – 20 · first Tue/Wed/Thu week

Timetable change. From this week the class meets on Tuesday, Wednesday and Thursday (announced in L9).

Readings for this week will be posted when the week begins.

L10. Software specifications; safety & liveness

Tue 18 Aug (Tue-4) · Topic 1
Slides
L10 — Software specifications (PDF)
Follow
Naik, “Software Specifications”, CIS 5470 (Penn); The Checker Framework manual
Paper
Outline
What a specification is and why there is nothing to test without one; kinds of specifications; pre- and post-conditions and weakest pre-conditions; contracts in testing vs verification; safety and liveness; typestate properties; types as lightweight specs and the Checker Framework; black-box vs white-box, automated vs manual testing.

L11. Hoare logic

Wed 19 Aug (Wed-4) · Topic 1
Slides
L11 — Hoare logic (PDF)
Follow
Svendsen, Hoare Logic and Model Checking (Cambridge), lectures 1–3
Paper
Hoare, “An Axiomatic Basis for Computer Programming”, CACM 12(10), 1969.
Outline
Program state and assertions; the Hoare triple {P} C {Q}; partial vs total correctness; inference rules for skip, assignment, sequence, conditional and consequence; the assignment rule read backwards; the while rule, loop invariants and the three proof obligations.

L12. Invariants & specification inference

Thu 20 Aug (Thu-4) · Topic 1
Slides
L12 — Invariants and specification inference (PDF)
Follow
Naik, “Software Specifications”, CIS 5470 (Penn); JML //@invariant / //@requires annotations
Paper
Flanagan, Leino, “Houdini, an Annotation Assistant for ESC/Java”, FME 2001; Ernst et al., “Dynamically Discovering Likely Program Invariants” (Daikon), TSE 2001.
Outline
Program, loop and class invariants; why validity is not enough — the useful invariant is the one implying the post-condition; inferring specifications instead of writing them; the Houdini algorithm (candidate invariants, refutation, workflow) on buggy and corrected programs; pros and cons.
Week 5 · Topic 1 → 2 — Coverage, mutation testing & fuzzingAug 25 & 27 · Wed 26 Aug holiday

Wed 26 Aug — no class (holiday).

Readings for this week will be posted when the week begins.

L13. Coverage & mutation testing

Tue 25 Aug (Tue-5) · Topic 1 → 2
Slides
L13 — Coverage & mutation testing (PDF)
Follow
Zhu, Hall, May, “Software Unit Test Coverage and Adequacy”, ACM CSUR 1997; Aho §9 (CFG background for branch coverage)
Paper
Jia, Harman, “An Analysis and Survey of the Development of Mutation Testing”, TSE 2011.
Outline
Test adequacy — when is a test suite “enough”; statement / line, branch, condition and MC-DC coverage; coverage on the CFG and what coverage does not tell you; instrumenting a program to measure it; mutation testing — mutation operators, mutants and the mutation score; killed vs surviving mutants; equivalent mutants and undecidability; cost and mutant-reduction techniques.

L14. Introduction to fuzzing

Thu 27 Aug (Thu-5) · Topic 2
Slides
L14 — Introduction to fuzzing (PDF)
Follow
FB “Introduction to Fuzzing” & “Greybox Fuzzing”; AFL technical whitepaper (M. Zalewski)
Paper
Miller, Fredriksen, So, “An Empirical Study of the Reliability of UNIX Utilities”, CACM 1990; Böhme, Pham, Roychoudhury, “Coverage-based Greybox Fuzzing as Markov Chain” (AFLFast), CCS 2016; Fioraldi et al., “AFL++”, WOOT 2020.
Outline
Random testing and the 1990 UNIX utilities study; blind vs mutation-based fuzzing; seeds, corpora and mutation operators; what counts as a bug — crashes, assertions and sanitizers (ASan / UBSan / MSan) as oracles; black-, white- and greybox fuzzing; coverage-guided greybox fuzzing (AFL, libFuzzer, AFL++); edge-coverage instrumentation and the coverage bitmap; corpus scheduling and power schedules.
Week 6 · Topic 2 → 3 — Fuzzing wrap-up; dataflow startsSep 2 – 3 · Tue 1 Sep Institute Day

Tue 1 Sep — no class (Institute Day).

Readings for this week will be posted when the week begins.

L15. Fuzzing (continued): grammar-based fuzzing & concurrency testing

Wed 2 Sep (Wed-6) · Topic 2
Slides, readings and outline posted when this lecture is delivered.

L16. Dataflow analysis: lattices & fixed points; reaching definitions

Thu 3 Sep (Thu-6) · Topic 3
Slides, readings and outline posted when this lecture is delivered.
Week 7 · Topic 3 — Classical dataflow, numeric domains & wideningSep 8 – 9 · Quiz 1 on Thu Sep 10
Readings for this week will be posted when the week begins.

Quiz 1 on Thu 10 Sep, 2:00 PM — covers Topics 1–3.

L17. Available expressions & very busy expressions

Tue 8 Sep (Tue-7) · Topic 3
Slides, readings and outline posted when this lecture is delivered.

L18. Live variables & DCE; interval analysis, widening & abstract interpretation

Wed 9 Sep (Wed-7) · Topic 3
Slides, readings and outline posted when this lecture is delivered.

Quiz 1

Thu 10 Sep 2026 · 2:00–2:55 PM · Room 5G4 · Thursday slot
Covers
Topics 1–3 (Foundations, Testing/Fuzzing, Dataflow) — definitions, algorithms, worked examples; closed book.
Mid-Semester ExaminationsSep 13 – 20
No classes. Mid-sem exam covers L1–L18 (Topics 1–3). Project proposal due Sun 20 Sep.
Week 8Sep 22 – 24
Readings for this week will be posted when the week begins.

L20

Wed 23 Sep (Wed-8) · Room 5G4, 3:00–3:55 PM
Title, topic and materials posted when this lecture is delivered.

L21

Thu 24 Sep (Thu-8)
Title, topic and materials posted when this lecture is delivered.
Week 9Sep 29 – Oct 1
Readings for this week will be posted when the week begins.

L22

Tue 29 Sep (Tue-9)
Title, topic and materials posted when this lecture is delivered.

L23

Wed 30 Sep (Wed-9)
Title, topic and materials posted when this lecture is delivered.

L24

Thu 1 Oct (Thu-9)
Title, topic and materials posted when this lecture is delivered.
Week 10Oct 6 – 8
Readings for this week will be posted when the week begins.

L25

Tue 6 Oct (Tue-10)
Title, topic and materials posted when this lecture is delivered.

L26

Wed 7 Oct (Wed-10)
Title, topic and materials posted when this lecture is delivered.

L27

Thu 8 Oct (Thu-10)
Title, topic and materials posted when this lecture is delivered.
Week 11Oct 13 – 14 · Industry Talk 2 on Thu Oct 15
Readings for this week will be posted when the week begins.

L28

Tue 13 Oct (Tue-11)
Title, topic and materials posted when this lecture is delivered.

L29

Wed 14 Oct (Wed-11)
Title, topic and materials posted when this lecture is delivered.
Week 12Oct 21 – 22
Readings for this week will be posted when the week begins.

L31

Wed 21 Oct (Wed-12)
Title, topic and materials posted when this lecture is delivered.

L32

Thu 22 Oct (Thu-12)
Title, topic and materials posted when this lecture is delivered.
Week 13Oct 27 – 29
Readings for this week will be posted when the week begins.

L33

Tue 27 Oct (Tue-13)
Title, topic and materials posted when this lecture is delivered.

L34

Wed 28 Oct (Wed-13)
Title, topic and materials posted when this lecture is delivered.

L35

Thu 29 Oct (Thu-13)
Title, topic and materials posted when this lecture is delivered.
Week 14Nov 4 · Industry Talk 3 on Tue Nov 3 · Quiz 2 on Thu Nov 5
Readings for this week will be posted when the week begins.

Quiz 2 on Thu 5 Nov, 2:00 PM — covers Topics 4–8.

L37

Wed 4 Nov (Wed-14) · Room 5G4, 3:00–3:55 PM
Title, topic and materials posted when this lecture is delivered.

Quiz 2

Thu 5 Nov 2026 · 2:00–2:55 PM · Room 5G4 · Thursday slot
Covers
Topics 4–8 (Pointer, Constraint-based, Types, SymExec, Test generation) — definitions, algorithms, worked examples; closed book.
Week 15Nov 10 & 11
Readings for this week will be posted when the week begins.

L38

Tue 10 Nov (Tue-15)
Title, topic and materials posted when this lecture is delivered.

L39

Wed 11 Nov (Wed-15) · Last teaching day
Title, topic and materials posted when this lecture is delivered.
Industry Talks · Three guest lectures before end-semSep – Nov 2026
Three guest lectures from industry practitioners, interleaved with regular lectures to give a working-engineer view of program analysis in real security/tooling teams. Format: 45 min talk + 10 min Q&A. Held in Room 5G4. Speakers & topics will be filled in as they confirm;

L19. Industry Talk 1

Tue 22 Sep 2026 · 4:00–4:55 PM · Room 5G4 ·
Speaker
TBA

L30. Industry Talk 2

Thu 15 Oct 2026 · 2:00–2:55 PM · Room 5G4 ·
Speaker
TBA

L36. Industry Talk 3

Tue 3 Nov 2026 · 4:00–4:55 PM · Room 5G4 ·
Speaker
TBA