Week 0: Introduction, Racket, and Metacircular Interpreters

  • M/W: Racket intro

Week 2: Metacircular interpers (contd), Lambda Calculus

  • Monday (labor day): No class
  • Wednesday: Metacircular Interpreters
  • Homework 0 handed out

Week 3: Lambda calculus, Church Encoding

  • Monday: Metacircular interpreters contd.
  • Wednesday: Lambda Calculus, Church Encoding

Week 4: Church Encoding and Continuations

  • Monday: Implementing the Church-encoder in class
  • Wednesday: Continuations, call/cc, and composable continuations
  • Homework 1 handed out (this Thursday / next Monday)

Week 5: Abstract machines (CEK and CESK) and Continuations

  • Monday: The CEK machine
  • Wednesday: Store-passing and the CESK machine

Week 6: Abstract Interpretation Basics

  • Monday: Abstract Interpretation theory and Galois Connections
  • Wednesday: Collecting Semantics and example abstract interpreter
  • Assigned reading: “Abstracting Abstract Machines.” http://matt.might.net/papers/vanhorn2010abstract.pdf

Week 7: Imperative Languages and Traditional Dataflow Analysis

  • Monday: Implementing IMP.
  • Wednesday: Implementing AAM in class.
  • Assigned reading: “Allocation Characterizes Polyvariance.” https://gilray.org/pdf/allocation-polyvariance.pdf

Week 9: Analysis Precision, Polyvariance

  • Monday: Context sensitivity, k-CFA
  • Wendesday: Polyvariance via Allocation
  • Assigned reading: “Resolving and Exploiting the k-CFA Paradox.” http://matt.might.net/papers/might2010mcfa.pdf

Week 10: Object-Orientation and Object Sensitivity

  • Monday: Encoding Objects as Flat Environments
  • Wednesday: m-CFA vs. k-CFA
  • Assigned reading: “Pick Your Contexts Well: Understanding Object-Sensitivity.” https://yanniss.github.io/typesens-popl11.pdf

Week 11: Reachability-based analysis

  • Monday / Wednesday:
  • Graph Reachability and IFDS
  • Assigned reading: Precise Interprocedural Dataflow Analysis via Graph Reachability

Week 12: Call/return matching, Pushdown precision

  • Monday: Pushdown Precision ala. Reps
  • Wednesday: Pushdown for Free.
  • Assigned reading: “Pushdown Control-Flow Analysis for Free.” http://matt.might.net/papers/gilray2016pushdown.pdf

Week 13: Constraint-Based Analyses

  • TBD

Week 14: Symbolic Execution

  • TBD

Week 15: Abstract Symbolic Execution and Abstracting Definitional Interpreters

  • Assigned Reading “Higher order symbolic execution for contract verification and refutation”
  • https://www.cambridge.org/core/services/aop-cambridge-core/content/view/129E10B4113242ABB0B7D6890CCFDBC9/S0956796816000216a.pdf/higher_order_symbolic_execution_for_contract_verification_and_refutation.pdf