| Date | Lecture | Reading | Homework (submit via Canvas) |
|---|---|---|---|
| Wed Jan 8 | Introduction | ||
| Fri Jan 10 | Static and dynamic analysis | notes chapter 1 and section 2.24 (Notes on "Static and dynamic analysis: synergy and duality"); Static and dynamic analysis: synergy and duality; Lessons from building static analysis tools at Google | |
| Tue Jan 14 | HW1: Development difficulties | ||
| Wed Jan 15 | Abstract interpretation | notes sections 2.0 - 2.14. | Exercises 4 and 5 from the notes |
| Fri Jan 17 | Abstract interpretation | notes rest of chapter 2; Abstract Interpretation: a semantics-based tool for program analysis sections 1.0-2.2; skim remainder of section 2. | Skim HW1 submissions and read those that interest you (nothing to submit); Exercises 15 and 16 (monotonicicy) and 26 and 27 (Stein's algorithm) from the notes |
| Wed Jan 22 | Abstract interpretation wrapup & demo | ||
| Thu Jan 23 | |||
| Fri Jan 24 | Project proposal and form groups; optional: read potential research projects (note 3 other lists of projects are linked from it) | ||
| Sat Jan 25 | Exercise 29 (divide by zero design) from the notes | ||
| Wed Jan 29 | Test generation | notes chapter 3 and section A.3 (Testing; terminology: Bugs, defects, and failures), Feedback-directed Random Test Generation, EvoSuite: Automatic Test Suite Generation for Object-Oriented Software | |
| Fri Jan 31 | Program repair | "A systematic study of automated program repair: fixing 55 out of 105 bugs for $8 each" | |
| Sat Feb 1 | Exercise 30 (divide by zero implementation) from the notes | ||
| Wed Feb 5 | Project presentations | slides (please use a light background for your slides) | |
| Fri Feb 7 | Program repair | "An Analysis of Patch Plausibility and Correctness for Generate-and-Validate Patch Generation Systems", "Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis" | report (related work and methodology complete) |
| Wed Feb 12 | Static slicing | "Program slicing" by Mark Weiser "Thin slicing", by Manu Sridharan, Stephen J. Fink and Ras Bodik, in PLDI 2007. |
|
| Fri Feb 14 | Dynamic slicing | Debugging Reinvented: Asking and Answering Why and Why Not Questions About Program Behavior by Amy J. Ko and Brad A. Myers, in ICSE '08, "Cost Effective Dynamic Program Slicing", by Xiangyu Zhang and Rajiv Gupta, in PLDI 2004. | report (address comments, add new text) |
| Wed Feb 19 | ML for SE | Neural software analysis, code2vec: learning distributed representations of code; visit the code2vec website. | |
| Fri Feb 21 | ML for SE | "Suggesting accurate method and class names". | report (address comments, add new text) |
| Wed Feb 26 | Model checking | Review linear temporal logic and buchi automaton; "CMC: a pragmatic approach to model checking real code" and "Finding and Reproducing Heisenbugs in Concurrent Programs". | |
| Fri Feb 28 | Project presentations | slides (please use a light background for your slides), report (code and initial results complete) | |
| Wed Mar 5 | Model checking | "The Model Checker SPIN", "Using predicate abstraction to reduce object-oriented programs for model checking", and "Counterexample-Guided Abstraction Refinement". | |
| Fri Mar 7 | Typestate | Typestate: A Programming Language Concept for Enhancing Software Reliability and Effective Typestate Verification in the Presence of Aliasing. | report (address comments, add new text) |
| Wed Mar 12 | No class (visit days) | ||
| Fri Mar 14 | Accumulation analysis | Chapter 3 of Lightweight Verification via Specialized Typecheckers, titled "Lightweight Verification via Accumulation Analysis." | report (address comments, add new text) |
| Wed Mar 19 | 2:30-4:30 Final Presentations | slides (please use a light background for your slides), report (final version) |