Lecture Material and Assignments

Lecture Material

• Lecture 1 - Introduction
• Lectures 2,3 - OCaml
• Lecture 4 - Symbolic execution
  • EXE: Automatically Generating Inputs of Death
  • (Optional) DART: Directed Automated Random Testing
  • (Optional) Mixing Type Checking and Symbolic Execution
• Lectures 5,6 - Data flow analysis
• Lecture 7 - Static Single Assignment Form
  • (Optional) Efficiently Computing Static Single Assignment Form and the Control Dependence Graph
• Lecture 8 - Software Foundations, Basics.v
• Lecture 9 - Lists.v, Poly.v, InClass1.v
• Lecture 10 - Software foundations, Ind.v, Logic.v
• Lecture 11 - Data flow analysis applications
  • ESP: path-sensitive program verification in polynomial time [slides]
  • Modular checking for buffer overflows in the large [slides, slides, and more slides]
• Lecture 12 - Software foundations, SfLib.v, Imp.v
• Lecture 13 - Software foundations, InClass3.v, Equiv.v
• Lecture 14 - Software foundations, InClass4.v, Rel.v, Smallstep.v, Lambda calculus
• Lecture 15 - Separation Logic
  • (Optional) Separation Logic: A Logic for Shared Mutable Data Structures
• Lecture 16 - Separation logic, lambda calculus
  • Lambda calculus exercises and solutions
• Lecture 17 - Type systems
• Lecture 18 - Andrew Myers, Programming secure, composable distributed systems with a higher-level language abstraction
• Lecture 19 - Type systems, Software foundations, Stlc.v
• Lecture 20 - Type systems, type-inf.ml
• Lectures 21-22 - Type qualifiers
  • (Optional) Flow-Insensitive Type Qualifiers
• Lecture 23 - How to give a research talk, How to write a research paper
• Lecture 24 - Software foundations, Hoare.v
• Lecture 25 - cancelled
• Lecture 26 -
• Lecture 27 (Dec 1) - Project presentations
  2. Amanda - Debugging a Program using Symbolic Execution
  1. Bryan and Brianna - Characterizing Bugs by Example in Support of Static Analysis
  3. Jinseong and Youngil - inversion Mobile. Case "Android". apply IHsecurePolicy...
  
• Lecture 28 (Dec 6) - Project presentations
  4. Mike and Tim - Dusting up Rubydust: Performance and Testing Improvements
  5. Teng and Arun - Acheiving Scalability in Configurable Software System Testing
  6. Khaled - Type Recovery in a Binary Rewriter
  7. Alison and Vikas - Formalization of Data Flow Analysis in Coq
• Lecture 29 (Dec 8) - Project presentations
  8. Ben and Greg - TeachRuby: Imperative Ruby for Introductory CS Curricula
  9. Brandyn - Automatically Generating Vision Algorithms Given Constraints
  10. Hsueh-Chien - Search Algorithms in Software Debugging and Testing

Assignments

• Project 1 - OCaml warmup
• Project 2 - Symbolic execution
• Project 3 - Exercises using Coq
• Project 4 - More exercises using Coq
• Project 5 - Stlc.v

Practice problems

Problems.