Schedule

Venue

Tuesdays at 2:30-4:20 in AQ 5018
Thursdays at 2:30-3:20 in SEC 1010

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 Representations Slicing 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 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 7	LLVM LLVM Demo		Barry Rosen, Mark Wegman, Kenneth Zadeck Global Value Numbers and Redundant Computations POPL 88 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 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 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
	Sep 28	Testing and Symbolic Execution		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
	Oct 5	Security		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 ASPLOS 2006
				Veselin Raychev, Martin Vechev, Manu Sridharan Effective race detection for event-driven programs OOPSLA 2013
	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 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
7	Oct 17	Test Case Reduction Project 4 due Oct 30		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
	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
8	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 OOPSLA 2016 Web Page
9	Nov 2		Alex, Ian	Gene Novark, Emery D. Berger DieHarder: Securing the Heap CCS 2010 Video
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
10	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
11	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
12	Nov 23		Faisal	Xiaozhu Meng, Barton P. Miller Binary Code Is Not Easy ISSTA 2016
13	Nov 28	PROJECT PRESENTATIONS
13	Nov 30	PROJECT PRESENTATIONS
14	Dec 5	Term Project Report Due