Program analysis
Graduate · CS / Programming
Syllabus focus
Theoretical / proof-based
Pricing
Graduate-level rates are set on consultation. See the pricing page for K–12 and undergraduate rates.
Topics typically covered
Theoretical / proof-based
Static analysis foundations
- Operational semantics and trace semantics
- Lattice theory and fixed-point theorems
- Abstract interpretation framework
- Live variables, available expressions, reaching definitions
- Widening and narrowing for termination
Advanced analyses
- Interprocedural analysis and call graphs
- Pointer analysis: Andersen vs Steensgaard (intro)
- Type systems and soundness proofs
- Model checking and symbolic execution (intro)
- Verification of concurrent programs (intro)
Research topics
- Separation logic for heap reasoning (intro)
- SMT solvers in verification workflows
- Bug finding in production compilers
- Reading PLDI/POPL papers
- Course project: implement an analysis pass
Notes
Graduate programming languages course; expects compilers and logic background.