Write a Blog >>
Tue 21 Jan 2020 10:30 - 11:10 at Ile de France III (IDF III) - Morning 2 Chair(s): Robbert Krebbers

SAT and Satisfiability Modulo Theories (SMT) solvers have many important applications in PL, including verification, testing, type checking and inference, and program analysis – but they are often a mysterious black box to their users, even when those users are PL researchers with lots of solver experience! This talk will be partly a tutorial introduction to the inner workings of SAT and SMT solvers, and partly an extended analogy to navigating life as a researcher: making decisions when you have only incomplete information to go on, learning from decisions that turned out to be bad, and determining when to give up and when to try again. I’ll also highlight a variety of papers in this year’s POPL program that make use of SAT and SMT solving, and discuss why I think it’s worthwhile to learn about solver internals.

Tue 21 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

10:30 - 12:30: PLMW 2020 - Morning 2 at Ile de France III (IDF III)
Chair(s): Robbert KrebbersDelft University of Technology
PLMW-POPL-202010:30 - 11:10
Lindsey KuperUniversity of California, Santa Cruz
Media Attached
PLMW-POPL-202011:10 - 11:50
Marco GaboardiBoston University
Media Attached File Attached
PLMW-POPL-202011:50 - 12:30
Xavier LeroyCollège de France
Media Attached File Attached