Course announcement: SMT Solving and Solver-Aided Systems

This fall, I’m teaching a graduate seminar on a topic I’m very excited about: the design and implementation of SMT solvers, solver-aided languages, and solver-aided systems!

SAT and SMT solvers are now widely used across many areas of computer science, especially for automated software and hardware verification, but they are often “black boxes” to their users. This course is for those who want to look under the hood to learn how solvers work, and to explore a variety of systems that make use of them.

The first few weeks of the course will focus on SAT and SMT solver internals and will have a lecture format, based on the first few chapters of Kroening and Strichman’s book. After that, it’ll become a more typical seminar course: students will read and present papers on interesting solvers (like STP and Reluplex), solver-aided languages (like Dafny, Liquid Haskell, Rosette, and Kaplan), and solver-aided systems (like KLEE, Indigo, and Quelea). Some questions I want to explore include:

• How does one design systems amenable to SMT-based verification?
• Can solver-aided languages help us build solver-aided systems?
• Under what circumstances are off-the-shelf SMT solvers too blunt or too slow of a hammer for a given problem? When should one build a custom solver, as opposed to trying to find the right way to encode a problem for an existing solver?
• How can we make it easier for domain experts to implement their own domain-specific solvers or solver extensions in high-level languages?

We’re also going to have at least two guest speakers, James Bornholt and Mangpo Phothilimthana, both experts on solver-aided systems. I’m looking forward to learning from both of them!

Students wanted!

If you’re a computer science grad student (or a grad student in something closely related to CS, or an ambitious undergrad) at UC Santa Cruz, check out the course overview and draft reading list, and consider signing up to take my class! (You can contact me to request a permission code if you need one.) And if you’re not a computer science grad student at UC Santa Cruz, but you think you want to be, then we should talk.