Current schedule of readings

This list is subject to change, and it is neither sound (i.e., if something’s listed here, that doesn’t mean we’ll read it) nor complete (i.e., if something’s not listed here, that doesn’t mean we won’t read it).

Links in the “Topic” column for the first three weeks of class link to lecture notes for those topics. After that, we’ll dispense with the lecture format and move to student presentations.

Date Topic Presenter Reading
Friday, 9/27 Course overview Lindsey (none)
Monday, 9/30 “The science of brute force” Lindsey Marijn J. H. Heule and Oliver Kullmann, The science of brute force (CACM 2017)
Wednesday, 10/2 Introduction to decision procedures, part 1 Lindsey Sections 1.0-1.3 (pp. 1-14) of Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, second edition (2016) (off-campus access link)
Friday, 10/4 Introduction to decision procedures, part 2 Lindsey Sections 1.4-1.7 (pp. 14-23) of Kroening and Strichman
Monday, 10/7 Introduction to SAT solving, part 1 Lindsey Sections 2.1-2.2.3 (pp. 27-38) of Kroening and Strichman
Wednesday, 10/9 Class cancelled due to power outage (please read lecture notes anyway)
Introduction to SAT solving, part 2		 Lindsey Sections 2.2.4-2.2.9 (pp. 38-50) of Kroening and Strichman
Friday, 10/11 Introduction to SMT solving Lindsey Sections 3.1-3.4 (pp. 59-72) of Kroening and Strichman
Monday, 10/14 Theories: Equality and uninterpreted functions Lindsey Sections 4.1-4.5 (pp. 77-91) of Kroening and Strichman
Wednesday, 10/16 Theories: Linear arithmetic Lindsey Sections 5.1-5.2 (pp. 97-106) of Kroening and Strichman
Friday, 10/18 Solver-aided systems Samuel Cristian Cadar et al., EXE: automatically generating inputs of death (CCS 2006)
Monday, 10/21 Solver design and implementation Will Vijay Ganesh and David L. Dill, A decision procedure for bit-vectors and arrays (CAV 2007) (off-campus access link)
Wednesday, 10/23 Solver design and implementation Clara Adam Kiezun et al., HAMPI: a solver for string constraints (ISSTA 2009)
Friday, 10/25 Solver-aided systems Matthew Cristian Cadar, Daniel Dunbar, and Dawson Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs (OSDI 2008)
Monday, 10/28 Class cancelled due to power outage    
Wednesday, 10/30 Solver-aided languages Akhil, David Richard Uhler and Nirav Dave, Smten with satisfiability-based search (OOPSLA 2014) (off-campus access link); Emina Torlak and Rastislav Bodik, Growing solver-aided languages with Rosette (Onward! 2013)
Friday, 11/1 Solver-aided systems (2-page project proposals due EOD) Guest lecture: Mangpo Phothilimthana (Google Brain) Phitchaya Mangpo Phothilimthana et al., Swizzle Inventor: Data Movement Synthesis for GPU Kernels (ASPLOS 2019)
Monday, 11/4 Solver design and implementation Zehui Cunjing Ge et al., SMT solving for the theory of ordering constraints (LCPC 2015) (off-campus access link)
Wednesday, 11/6 Solver-aided languages Gan Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala, Liquid types (PLDI 2008) (off-campus access link)
Friday, 11/8 Solver-aided languages Akhil K. Rustan M. Leino, Dafny: an automatic program verifier for functional correctness (LPAR 2010) (off-campus access link)
Monday, 11/11 No class (Veterans Day)    
Wednesday, 11/13 Class cancelled due to strike    
Friday, 11/15 Solver-aided languages Guest lecture: James Bornholt (UT Austin) James Bornholt and Emina Torlak, Finding code that explodes under symbolic evaluation (OOPSLA 2018)
Monday, 11/18 Solver-aided languages (Project status update week begins) Matthew, Gan Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter, Constraints as control (POPL 2012) (off-campus access link); Niki Vazou et al., Refinement types for Haskell (ICFP 2014) (off-campus access link)
Wednesday, 11/20 Solver-aided systems David Valter Balegas et al., Putting consistency back into eventual consistency (EuroSys 2015) (off-campus access link)
Friday, 11/22 Solver-aided systems (Project status update week ends) Clara KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan, Declarative Programming over Eventually Consistent Data Stores (PLDI 2015)
Monday, 11/25 Solver-aided systems Zehui Pavel Panchekha and Emina Torlak, Automated reasoning for web page layout (OOPSLA 2016)
Wednesday, 11/27 Solver design and implementation Will Guy Katz et al., Reluplex: an efficient SMT solver for verifying deep neural networks (CAV 2017) (extended version on arXiv)
Friday, 11/30 No class (Thanksgiving)    
Monday, 12/2 Solver-aided systems Samuel Luke Nelson et al., Hyperkernel: push-button verification of an OS kernel (SOSP 2017)
Wednesday, 12/4 15-minute project presentations Zehui, Will, David, Gan  
Friday, 12/6 15-minute project presentations (Project reports due EOD) Samuel, Clara, Matthew, Akhil  
Thursday, 12/12 final exam end-of-quarter celebration at 10am (special location: the LSD lab (Engineering 2, Room 398))  

Further reading

The first three weeks

We’ll mostly assume that you are familiar with the basics of propositional logic, but if you need a refresher, look at Chapter 1 (Propositional Logic) of The Calculus of Computation: Decision Procedures with Applications to Verification (2007) by Aaron R. Bradley and Zohar Manna (off-campus access link). Bradley and Manna’s book is also a good alternative resource for many of the other topics covered in Kroening and Strichman.

The Handbook of Satisfiability (2009) (off-campus access link to online edition), edited by A. Biere, M. Heule, H. van Maaren, and T. Walsh, is an excellent reference for many topics we’ll be covering in the first three weeks of class.

A couple of slightly older CACM articles, in addition to the one we have as an assigned reading, provide an approachable overview of SAT and SMT:

Many solver-aided languages and systems rely on the Z3 SMT solver. The standard citation is: Leonardo de Moura and Nikolaj Bjørner, Z3: an efficient SMT solver (TACAS 2008) (off-campus access link). If you want to become familiar with Z3, check out the tutorial and interactive guide.

Are you bored of academic papers about SMT? Dennis Yurichev’s SAT/SMT by Example is impressive and fun.

The rest of the course

There’s a vast amount of reading material that would be in scope for a course on SMT solving and solver-aided systems, but that this particular course won’t have time to cover, including but not limited to: