Schedule

Venue

Tuesdays at 10:30-11:20 in AQ 3003
Thursdays at 9:30-11:20 in WMC 3260

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 9:00PM before the class (PDFs, please).

The schedule is subject to change.

Week	Date	Topics	Papers
1	Sep 4	Introduction Representations Slicing Notes on CSIL Project 1 due Sep 17		Yannis Smaragdakis, George Balatsouras Pointer Analysis
				Jeanne Ferrante, Karl Ottenstein, Joe Warren The Program Dependence Graph and Its Use in Optimization TOPLAS 1987
				Mark Weiser Program Slicing TSE 1984
				Susan Horwitz, Thomas Reps, David Binkley Interprocedural slicing using dependence graphs PLDI 88 Retrospective
				Hiralal Agrawal Dynamic Program Slicing PLDI 90 Computing them efficiently
				Frank Tip A Survey of Program Slicing Techniques
	Sep 6	LLVM LLVM Demo Reading due Today		Barry Rosen, Mark Wegman, Kenneth Zadeck Global Value Numbers and Redundant Computations POPL 88 Commentary on developing SSA
2	Sep 11	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 TOPLAS 2016
				Todd Mytkowicz, Amer Diwan, Matthias.Hauswirth, Peter Sweeney Producing wrong data without doing anything obviously wrong! ASPLOS 2009
				Konstantin Serebryany, Derek Bruening, Alexander Potapenko, Dmitriy Vyukov AddressSanitizer: a fast address sanity checker Usenix ATC 2012
	Sep 13	Formal Tools Read through Ch4 due Today		Philip Wadler A taste of linear logic
				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
				Stephane Demri, Morgan Deters Logical Investigations on Separation Logics
				Alexis Beingessner The Pain Of Real Linear Types in Rust
				Phil Gossett Parametric Polymorphism and the Girard-Reynolds Isomorphism
3	Sep 18	Static Analysis Project 2 due Oct 1		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
	Sep 20	Static Analysis		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
4	Sep 25	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
	Sep 27	Testing and Symbolic Execution		Koushik Sen, Christian Cadar Symbolic Execution for Software Testing: Three Decades Later CACM, February 2013 Efficient Encodings Counterpoints from fuzzing
	Sep 27	Testing and Symbolic Execution		Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, Irene Finocchi A Survey of Symbolic Execution Techniques
5	Oct 2	Security Project 3 due Oct 15		Nathan Burow, Scott A. Carr, Joseph Nash, Per Larsen, Michael Franz, Stefan Brunthaler, Mathias Payer Control-Flow Integrity: Precision, Security, and Performance CSUR 2017
	Oct 2	Security Project 3 due Oct 15		Nicolas Carlini, Antonio Barresi, Mathias Payer, David Wagner, Thomas R. Gross Control-Flow Bending: On the Effectiveness of Control-Flow Integrity Usenix Security 2015
	Oct 4	Parallelism and Concurrency		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 ASPLOS 2006
				Veselin Raychev, Martin Vechev, Manu Sridharan Effective race detection for event-driven programs OOPSLA 2013
6	Oct 9	Synthesis Term Project Proposal due Oct 9		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 TOPLAS 1980
				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
	Oct 11	Test Case Reduction Project 4 due Oct 29		Andreas Zeller, Ralf Hildebrandt Simplifying and isolating failure-inducing input. TSE 2002 Commentary
				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
7	Oct 16		Eleanor	Caroline Lemieux, Rohan Padhye, Koushik Sen, Dawn Song PerfFuzz: Automatically Generating Pathological Inputs ISSTA 2018 GitHub Evaluating Fuzz Testing Blog post for above paper
7	Oct 18		Brendan	Peng Chen, Hao Chen Angora: Efficient Fuzzing by Principled Search Security & Privacy
8	Oct 23		Wilson	Chengnian Sun, Vu Le, Zhendong Su Finding Compiler Bugs via Live Code Mutation OOPSLA 2016 EMI & SPE Compiler Testing
8	Oct 25		Cole & Oscar	Amin Milani Fard, Ali Mesbah Feedback-Directed Exploration of Web Applications to Derive Test Models ISSRE 2013 GitHub
9	Oct 30		Jordan	Michael Schwarz, Martin Schwarzl, Moritz Lipp, Daniel Gruss NetSpectre: Read Arbitrary Memory over Network N/A Spectre: Secrets, Side-Channels, Sandboxes, and Security Hello from the Other Side: SSH over Robust Cache Covert Channels in the Cloud
9	Nov 1		Alex	Rifat Shahriyar, Stephen M. Blackburn, Daniel Frampton Down for the Count? Getting Reference Counting Back in the Ring ISMM 2012 Jikes RVM RC Immix
10	Nov 6		Liam	Emina Torlak, Ras Bodik Growing solver-aided languages with rosette Onward! 2013 Rosette Project A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages A Programmable Programming Language
10	Nov 8		Sean	Dennis Brylow Niels Damgaard, Jens Palsberg Static Checking of Interrupt-driven Software ICSE 2001 HOIST: A System for Automatically Deriving Static Analyzers for Embedded Systems Modular Verification of Interrupt-Driven Software FirmUp: Precise Static Detection of Common Vulnerabilities in Firmware
11	Nov 13		Chuck	Sebastian Vogl, Robert Gawlik, Behrad Garmany, Thomas Kittel, Jonas Pfoh, Claudia Eckert, Thorsten Holz Dynamic Hooks: Hiding Control Flow Changes within Non-Control Data USENIX Security 2014
11	Nov 15		Kia	Uri Alon, Meital Zilberstein, Omer Levy, Eran Yahav A General Path-Based Representation for Predicting Program Properties PLDI 2018 GitHub Project Page Code2Vec
12	Nov 20		Navid	Jason Ansel, Shoaib Kamil, Kalyan Veeramachaneni, Jonathan Ragan-Kelley, Jeffrey Bosboom, Una-May O’Reilly, Saman Amarasinghe OpenTuner: An Extensible Framework for Program Autotuning PACT 2014
12	Nov 22		Mahsa	Haojie Wang, Jidong Zhai, Xiongchao Tang, Bowen Yu, Xiaosong Ma, Wenguang Chen Spindle: Informed Memory Access Monitoring USENIX ATC 2018 GitHub
13	Nov 27	PROJECT PRESENTATIONS	Chuck
			Jordan
			Mahsa
			Navid
	Nov 29	PROJECT PRESENTATIONS	Brendan
			Kia
			Eleanor
			Liam
			Sean
			Alex
			Wilson
			Oscar/Cole
14	Dec 4	Term Project Report Due