Everyone should have read the paper before class. Presenters mayshould assume people have read the paper, and focus their presentation on clarifying or explroing the material (e.g., through worked examples, developing intuition for definitions. etc) rather than on, e.g., re-iterating motivation already covered by the paper.

Presenters should send to the class a brief "homework" about not less than four days before presenting. Homework comes in a variety of forms---a section to read with a concrete question to answer in mind, a concrete example to work out, a hypothetical extension to the system, a quick experiment using an online tool (factor download/install time into the assignment)---but should not take more than thirty or forty minutes to do.

When you present, you can assume that everyone has done the homework. It may be good to give the "right" answer, in case not everyone figured it out.

NOTE: Schedule is subject to change.

Lec.	Date	Topic	Notes/Readings
Decision Procedures/Applied Logic
1	Tue 29-Jan	Intro to SMT	Presenter: Ming Z3: An efficient SMT solver. Leonardo De Moura and Nikolaj Bjorner. TACAS 2008.
2	Thu 31-Jan
3	Tue 5-Feb	Horn clauses	Presenter: Aaron On Solving Universally Quantified Horn Clauses. Nikolaj Bjorner, Ken McMillan, and Andrey Rybalfchenko. SAS 2013.
4	Thu 7-Feb	Separation Logic	Presenter: David Separation Logic: A Logic for Shared Mutable Data Structures. John Reynolds. LICS 2002.
5	Tue 12-Feb		Presenter: Eric Propagation based local search for bit-precise reasoning. Aina Niemetz, Mathias Preiner, Armin Biere. Journal of Formal Methods in System Design, 5(3), 2017.
Synthesis
6	Thu 14-Feb		Presenter: Michael FlashMeta: A Framework for Inductive Program Synthesis. Oleksandr Polozov and Sumit Gulwani. OOPSLA 2015.
7	Tue 19-Feb		Presenter: David User-Guided Device Driver Synthesis. Ryzhyk, Walker, Keys, Legg, Raghunath, Stumm, and Vij. OSDI 2014.
8	Thu 21-Feb		Presenter: Basu Tortoise: Interactive System Configuration Repair. Aaron Weiss, Arjun Guha, and Yuriy Brun. ASE 2017.
9	Tue 26-Feb		Presenter: Teddy Type-and-Example-Directed Program Synthesis. Peter-Michael Osera and Steve Zdancewic. PLDI 2015. Program Synthesis from Polymorphic Refinement Types. Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama. PLDI 2016.
10	Thu 28-Feb		Presenter: Eric Structuring the Synthesis of Heap-Manipulating Programs. Nadia Polikarpova and Ilya Serge. POPL 2019.
ISA Semantics
11	Tue 5-Mar		Presenter: Crystal ISA Semantics for ARMv8-A, RISC-V and CHERI-MIPS. Armstrong, Bauereiss, Campbell, Reid, Gray, Norton, Mundkur, Wassell, French, Pulte, Flur, Stark, Krishnaswami, and Sewell. POPL 2019.
12	Thu 7-Mar		Path-Exploration Lifting: Hi-Fi Tests for Lo-Fi Emulators. Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. ASPLOS 2012.
Information Flow
13	Tue 12-Mar		Presenter: Marcy Types for Information Flow Control: Labeling Granularity and Semantic Models. Rajani and Garg, CSF 2018.
14	Thu 14-Mar		Presenter: Alex From Fine- to Coarse-Grained Dynamic Information Flow Control and Back. Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan. POPL 2019.
Spring Recess
Types
15	Tue 26-Mar		Presenter: Teddy Stitch: The Sound Type-Indexed Type Checker. Richard A. Eisenberg.
16	Thu 28-Mar		Presenter: Jian Type Soundness for Dependent Object Types. Tiark Rompf and Nada Amin. OOPSLA 2016.
17	Tue 2-Apr		Presenter: Marcy A Theory of Type Coercions and its Applications. Nikhil Swamy, Michael Hicks, and Gavin Bierman. ICFP 2009.
HOAS
18	Thu 4-Apr		Presenter: Richard Higher-order abstract syntax. Frank Pfenning, and Conal Elliott. POPL 1988.
19	Tue 9-Apr		Presenter: Aaron A logic programming approach to manipulating formulas and programs. Dale Miller and Gopalan Nadathur. SLP 1987.
Program Analysis
20	Thu 11-Apr		Presenter: Basu From Datalog to Flix: a declarative language for fixed points on lattices. Magnus Madsen, Ming-Ho Yee, and Ondrej Lhotak. PLDI 2016.
21	Tue 16-Apr		Presenter: Jian Incrementalizing lattice-based program analyses in Datalog. Tamas Szabo, Gabor Bergmann, Sebastian Erdweg, and Markus Voelter. OOPSLA 2018.
22	Thu 18-Apr		Presenter: Alex Finding Code That Explodes Under Symbolic Execution. James Bornholt and Emina Torlak, OOPSLA 2018.
Verified and Secure Compilation
23	Tue 23-Apr		Presenter: Richard A Verified Compiler for an Impure Functional Language. Adam Chlipala. POPL 2010.
24	Thu 25-Apr		Presenter: Crystal? A Verified, Efficient Embedding of a Verifiable Assembly Language. Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. POPL 2019.
25	Tue 30-Apr		Project presenatations.