E0 327 Topics in Program Analysis

• Course outline
  • Program Logics for Heaps/Arrays
    • Shape analysis [Slides, Assignment, Solution]
    • Separation logic [Assignment]
    • Lifting Abstract Interpreters to Quantified Logical Domains [Slides, Assignment]
  • Pointer Analysis
    • Parameterized object sensitivity for points-to analysis for Java [Slides, Assignment]
    • Refinement-Based Context-Sensitive Points-To Analysis for Java [Slides]
  • Verification via Symbolic Execution and Predicate Abstraction
    • Slam/Blast [Slam papers Overview, C2BP, Bebop, Newton.]
    • Blast slides [Slides]
    • Slam slides [Slides]
  • Concurrency
    • Owicki-Gries
    • Rely-Guarantee
    • Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs
  • Type Systems
    • Type-based flow analysis [Slides, Assignment]
    • Dependent types in practical programming [Assignment] [Slides] [Other stuff]