If there are papers listed for a given day, you should read them before class that day. For student presented papers, on any week that you are not presenting a paper, you should write a response/critique to one of that week's papers. These critiques don't just show that you have at least skimmed through the paper, but they prepare you to discuss the papers and raise (or answer) questions during class. Critiques must be submitted via CourSys by 9:00PM before (PDFs, please). If you are presenting a paper, slides for presentation must be submitted via CourSys by 10:00PM before the class (PDFs, please).

The schedule is subject to change.

Week Date Topics Papers
1 Sep 5 Introduction
Notes on CSIL
Project 1 due Sep 18
Yannis Smaragdakis, George Balatsouras
Pointer Analysis
Jeanne Ferrante, Karl Ottenstein, Joe Warren
The Program Dependence Graph and Its Use in Optimization
Mark Weiser
Program Slicing
TSE 1984
Susan Horwitz, Thomas Reps, David Binkley
Interprocedural slicing using dependence graphs
Hiralal Agrawal
Dynamic Program Slicing
Computing them efficiently
Frank Tip
A Survey of Program Slicing Techniques
Sep 7 LLVM
Barry Rosen, Mark Wegman, Kenneth Zadeck
Global Value Numbers and Redundant Computations
Commentary on developing SSA
2 Sep 12 Dynamic Analysis Thomas Ball, James Larus
Efficient Path Profiling
MICRO 1996
Stephen M. Blackburn, Amer Diwan, Matthias Hauswirth, Peter F. Sweeney, Jose Nelson Amaral, Tim Brecht, Lubomr Bulej, Cliff Click, Lieven Eeckhout, Sebastian Fischmeister, Daniel Frampton, Laurie J. Hendren, Michael Hind, Antony L. Hosking, Richard E. Jones, Tomas Kalibera, Nathan Keynes, Nathaniel Nystrom, and Andreas Zeller
The Truth, The Whole Truth, and Nothing But the Truth: A Pragmatic Guide to Assessing Empirical Evaluations
Todd Mytkowicz, Amer Diwan, Matthias.Hauswirth, Peter Sweeney
Producing wrong data without doing anything obviously wrong!
Konstantin Serebryany, Derek Bruening, Alexander Potapenko, Dmitriy Vyukov
AddressSanitizer: a fast address sanity checker
Usenix ATC 2012
Sep 14 Static Analysis Anders Møller, Michael Schwartzbach
Static Program Analysis
Patrick Cousot, Radhia Cousot
Static Verification of Dynamic Type Properties of Variables
Patrick Cousot, Radhia Cousot
Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
POPL 1977
David A. Schmidt
Data flow analysis is model checking of abstract interpretations
POPL 1998
3 Sep 19 Static Analysis
Project 2 due Oct 2
Micha Sharir, Amir Pnueli
Two Approaches to Precise Interprocedural Dataflow Analysis
Program Flow Analysis: Theory and Practice
Full Report
Florian Martin
Experimental Comparison of Call String and Functional Approaches to Interprocedural Analysis
CC 1999
Ravi Mangal, Mayur Naik, Hongseok Yang
A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join
ESOP 2014
Sep 21 Static Analysis Thomas Reps, Susan Horwitz, Mooly Sagiv
Precise Interprocedural Dataflow Analysis via Graph Reachability
POPL 1995
John Kodumal, Alex Aiken
The Set Constraint/CFL Reachability Connection in Practice
PLDI 2004
Qirun Zhang, Michael R. Lyu, Hao Yuan, Zhendong Su
Fast Algorithms for Dyck-CFL-Reachability with Applications to Alias Analysis
PLDI 2013
Eric Bodden
Inter-procedural Data-flow Analysis with IFDS/IDE and Soot
4 Sep 26 Formal Tools
(class starts 30 min. late)
Emina Torlak
A Primer on Satisfiability
Thomas W. RepsMooly SagivReinhard Wilhelm
Static Program Analysis via 3-Valued Logic
CAV 2004
Peter O'Hearn
A Primer on Separation Logic
Why Separation Logic Works
Sep 28 Testing and Symbolic Execution Koushik Sen, Christian Cadar
Symbolic Execution for Software Testing: Three Decades Later
CACM, February 2013
Efficient Encodings
Counterpoints from fuzzing
Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, Irene Finocchi
A Survey of Symbolic Execution Techniques
5 Oct 3 NO CLASS
(term project planning)
Project 3 due Oct 16
Oct 5 Security Nathan Burow, Scott A. Carr, Joseph Nash, Per Larsen, Michael Franz, Stefan Brunthaler, Mathias Payer
Control-Flow Integrity: Precision, Security, and Performance
CSUR 2017
Nicolas Carlini, Antonio Barresi, Mathias Payer, David Wagner, Thomas R. Gross
Control-Flow Bending: On the Effectiveness of Control-Flow Integrity
Usenix Security 2015
6 Oct 10 Parallelism and Concurrency
Term Project Proposal due Oct 10
Leslie Lamport
Time, Clocks and the Ordering of Events in a Distributed System
CACM 1978
Also see Vector Clocks
Cormac Flanagan, Stephen Freund
Atomizer: A Dynamic Atomicity Checker For Multithreaded Programs
POPL 2004
Shan Lu, Joseph Tucek, Feng Qin, Yuanyuan Zhou
Avio: AVIO: Detecting Atomicity Violations via Access Interleaving Invariants
Veselin Raychev, Martin Vechev, Manu Sridharan
Effective race detection for event-driven programs
Oct 12 Synthesis Ras Bodik
Program synthesis: opportunities for the next decade
ICFP 2015 (Keynote)
Rosette Project, Synthesis Course
Zohar Manna, Richard Waldinger
A deductive approach to program synthesis
Rajeev Alur, Ras Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa
Syntax-guided synthesis
FMCAD 2013 (and extended version)
Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari
Oracle-Guided Component-Based Program Synthesis
ICSE 2010
Peter-Michael Osera, Steve Zdancewic
Type-and-Example-Directed Program Synthesis
PLDI 2015
7 Oct 17 Test Case Reduction
Project 4 due Oct 30
Andreas Zeller, Ralf Hildebrandt
Simplifying and isolating failure-inducing input.
TSE 2002
Ghassan Misherghi, Zhendong Su
HDD: Hierarchical Delta Debugging
ICSE 2006
John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang
Test-Case Reduction for C Compiler Bugs
PLDI 2012
Project Page
Oct 19 Pranav, Shadi Manu Jose, Rupak Majumdar
Cause Clue Clauses: Error Localization using Maximum Satisfiability
PLDI 2011
Web Page
8 Oct 24 Alex, Eric Mingxing Zhang, Yongwei Wu, Shan Lu, Shanxiang Qi, Jinglei Ren, Weimin Zheng
AI: A Lightweight System for Tolerating Concurrency Bugs
FSE 2014
On Github
Oct 26 Jiaxun, Ruoyi Chenglong Wang, Alvin Cheung, Rastislav Bodik
Synthesizing Highly Expressive SQL Queries from Input-Output Examples
PLDI 2017
Web page
9 Oct 31 Andrei, James Pavel Panchekha, Emina Torlak
Automated Reasoning for Web Page Layout
Web Page
Nov 2 Alex, Ian Gene Novark, Emery D. Berger
DieHarder: Securing the Heap
CCS 2010
10 Nov 7 Thai, Yu Hong Hu, Shweta Shinde, Sendroiu Adrian, Zheng Leong Chua, Prateek Saxena, Zhenkai Liang
Data-Oriented Programming: On the Expressiveness of Non-Control Data Attacks
Security and Privacy 2016
Web Page
Nov 9 Ao, Jiaqi Pavel Panchekha, Alex Sachez-Stern, James R. Wilcox, Zachary Tatlock
Automatically Improving Accuracy for Floating Point Expressions
PLDI 2015
Web page
11 Nov 14 Arthur, Bernard Azadeh Farzan, Victor Nicolet
Synthesis of Divide and Conquer Parallelism for Loops
PLDI 2017
On Github
Nov 16 NoorUllah, Savio Tianxiao Gu, Chengnian Sun, Xiaoxing Ma, Jian Lü, Zhendong Su
Automatic runtime recovery via error handler synthesis
ASE 2016
Web page
12 Nov 21 Shreeasish Dasarath Weeratunge, Xiangyu Zhang, William N. Sumner, Suresh Jagannathan
Analyzing Concurrency Bugs using Dual Slicing
ISSTA 2010
Nov 23
14 Dec 5 Term Project Report Due