# Readings

## 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).

Date | Topic | Presenter | Reading |
---|---|---|---|

Friday, 9/27 | Course overview | Lindsey | (none) |

Monday, 9/30 | The big picture | Lindsey | Marijn J. H. Heule and Oliver Kullmann, The science of brute force (CACM 2017) |

Wednesday, 10/2 | Introduction to decision procedures | 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 | Lindsey | Sections 1.4-1.7 (pp. 14-23) of Kroening and Strichman |

Monday, 10/7 | Introduction to SAT solving | Lindsey | Sections 2.1-2.2.3 (pp. 27-38) of Kroening and Strichman |

Wednesday, 10/9 | Introduction to SAT solving | 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.3 (pp. 97-111) and 5.7 (pp. 126-128) of Kroening and Strichman |

Friday, 10/18 | Solver design and implementation | Sam | 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 | Solver-aided languages | Akhil | Richard Uhler and Nirav Dave, Smten with satisfiability-based search (OOPSLA 2014) (off-campus access link) |

Wednesday, 10/30 | Solver-aided languages | David | 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 | Solver-aided languages (Project status update week begins) |
Matthew | Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter, Constraints as control (POPL 2012) (off-campus access link) |

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 | Gan | 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/3 | Solver-aided systems | Sam | Luke Nelson et al., Hyperkernel: push-button verification of an OS kernel (SOSP 2017) |

Wednesday, 12/4 | Project presentations | TBD | |

Friday, 12/6 | Project presentations (Project reports due EOD) |
TBD | |

Thursday, 12/12 | (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:

- Sharad Malik and Lintao Zhang, Boolean satisfiability: from theoretical hardness to practical success (CACM 2009)
- Leonardo de Moura and Nikolaj Bjørner, Satisfiability modulo theories: introduction and applications (CACM 2011) (off-campus access link)

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:

- …material on answer set programming systems with integrated solvers, such as:
- Martin Gebser et al., Potassco: the Potsdam answer set solving collection (
*AI Communications*, 2011) (off-campus access link) (see also: the Potassco website)

- Martin Gebser et al., Potassco: the Potsdam answer set solving collection (
- …more work on solver-based superoptimizing compilers, such as these papers (which are John Regehr’s and JF Bastien’s recommendations):
- Sorav Bansal and Alex Aiken, Automatic generation of peephole superoptimizers (ASPLOS 2006)
- Sumit Gulwani et al., Synthesis of loop-free programs (PLDI 2011) (off-campus access link)
- Sebastian Buchwald, OPTGEN: a generator for local optimizations (CC 2015) (off-campus access link)
- Eric Schkufza, Rahul Sharma, and Alex Aiken, Stochastic superoptimization (ASPLOS 2013)

- …more work on integration between a language and a solver, such as:
- Emina Torlak and Rastislav Bodik, A lightweight symbolic virtual machine for solver-aided host languages (PLDI 2014) (the follow-up to the Onward 2013 Rosette paper we’re reading)
- Aaron Bembenek and Stephen Chong, FormuLog: Datalog for static analysis involving logical formulae (2018)
- Trevor Elliott et al., Guilt free Ivory (Haskell Symposium 2015) (off-campus access link)
- William T. Hallahan, Anton Xue, and Ruzica Piskac, G2Q: Haskell constraint solving (Haskell Symposium 2019)

- …more work on solver design and implementation, such as:
- Robert Brummayer and Armin Biere, Boolector: an efficient SMT solver for bit-vectors and arrays (TACAS 2009) (see also: many related publications from the Boolector team)

- …more work on solver-aided systems for ensuring consistency in distributed systems, such as:
- Farzin Houshman and Mohsen Lesani, Hamsaz: replication coordination analysis and synthesis (POPL 2019)

- solver-aided systems for bug-finding and fault injection, such as:
- Peter Alvaro, Joshua Rosen, and Joseph M. Hellerstein, Lineage-driven fault injection (SIGMOD 2015)

- …follow-up work on Reluplex, such as:
- …recent creative applications of SMT solvers across subfields of CS, such as:
- Emma Tosch et al., PlanAlyzer: assessing threats to the validity of online experiments (OOPSLA 2019)
- Gabrielle Beck, Maximilian Zinkus, and Matthew Green, Using SMT solvers to automate chosen ciphertext attacks (2019)

- Etc., etc., etc.