Lecture Material and Assignments

Lecture Material

• Lecture 1 - Introduction (slides)
• Lectures 2,3 - OCaml (slides)
• Lecture 4 - Symbolic execution (slides, interpreter code)
  • (Optional) EXE: Automatically Generating Inputs of Death
  • For reference, see lectures 3 and 6 of this tutorial by Patrice Godefroid
  • (Optional) Directed Symbolic Execution
  • (Optional) DART: Directed Automated Random Testing
  • (Optional)Mixing Type Checking and Symbolic Execution
• Lectures 5,6 - Data flow analysis (slides)
  • (Optional) Efficiently Computing Static Single Assignment Form and the Control Dependence Graph
• Lecture 7 - Operational semantics (slides updated 2/18/13)
• Lecture 8,9 - Abstract Interpretation (slides updated 220, 8:15pm)
  • (Optional) Abstract interpretation tutorial (sections 1 and 2 recommended)
  • Example code for signs domain and IMP language: absinterp.tgz
  • (Optional) Introductory slides by Patrick Cousot
  • (Optional) Systematic Design of Program Analysis Frameworks, Cousot and Cousot
• Lecture 10 - Probabilistic Computation
• Some examples, concrete operational semantics (slides)
• Probabilistic abstract interpretation applied to knowledge-based security policies (slides, paper)
• Lecture 11 - Synthesis (slides)
• Lecture 12 - Lambda Calculus (slides)
• Lecture 13,14,15 - Types and Proofs (slides, sample typechecker, proof of STLC soundness)
• Lecture 16 - Dynamic Typing, Contracts, and Gradual Typing (slides)
• Lecture 16 - Dependent Types (notes)
• Lecture 17,18 - Coq
  • See the resources page for links to the Coq distribution, and Proof General
  • Course material for Coq: from Software Foundations
  • Coq lecture 1/2: Basics
  • Coq lecture 2/2: Lists, Poly, Gen, Prop and Logic.
• Lecture 19 - Axiomatic semantics (slides)
• Lecture 20 - Hoare Logic in Coq (Imp and Hoare)
• Lecture 21 - Language-Based Security
  • Introduction and Secure Information Flow
  • (Optional) Language-based information flow security
• Lecture 22 - Type qualifiers (as applied to security)
  • TOPLAS paper on general technique
  • USENIX Security paper on application to format strings
  • PLAS paper on application to entire Debian distribution
• Lecture 23 - Incremental computation
• Lecture 24 - Scriptable debugging (guest lecture from Khoo Yit Phang)
• Project presentations
  • How to write a research paper and How to give a research talk
• May 1:
  • Travis Brown, Fay and Effects: Safer JavaScript FFI.
  • Chris Imbriano and Chang Liu, Coq Formalization of Memory Trace Oblivious Execution.
  • Moshe Katz, Specification-Driven Implementation of Dynamically-Reconfigurable Distributed Applications.
  • Alex Malozemoff, Automatically Verifying and Synthesizing Cryptographic Modes of Operation.
  • Nate Parsons, Type Inference for M3PC, a Language for Mixed Mode Multiparty Computation.
  • Darren Smith, Compact Code Encodings.
• May 6:
  • William Armstrong, A Comparison of Automated Static Analysis Tools for use in Bug-detection on Stand-Alone Java Applications.
  • Cody Buntain, Automated Software Diversification via Synthesis-Based Metamorphism.
  • Yehuda Katz, Identifying and Analyzing Program Runtime Configuration.
  • Youndo Lee, A Survey on Static Analysis of SQL Queries.
  • Max Potasznik, Programming Languages in Software Defined Networks.
  • Anilesh Shrivastava, A Look at an Implementation of Probabilistic Abstract interpretation.
• May 8
  • Kerry Cheng and Rob Argue, Probabilistic Computation: Abstract Interpretation and Machine Learning.
  • Wenshuai Hou, A Survey on MapReduce and Its Variations.
  • Beth McNany and David Wasser, Symbolic Execution in Ruby.
  • Nuttiiya Seekhao and Hui Zhang, Synthesizing Distributed Memory Parallel Programs.

Homework

• Homework 1 - Dataflow analysis
• Homework 2 - Operational semantics and abstract interpretation
• Homework 3 - Type systems
• Homework 4 - Formal reasoning in Coq (requires Sflib.v)

Projects

• Programming project 1 - Ocaml programming
• Programming project 2 - Symbolic execution