- 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
Week 14: Symbolic Execution
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