| Lecture Title
| Lecturer
| Affiliation
|
|
| Category 1: Foundational Aspects of SAT/SMT Solvers |
Independence Results for the P vs. NP Question
|
Shai Ben David
|
University of Waterloo, Ontario, Canada
|
| Foundations of Modern CDCL SAT Solver Implementation
| Niklas Een
| University of California, Berkeley, USA |
| SMT Theory and DPLL(T)
| Albert Oliveras
| Technical Univ. of Catalonia, Barcelona, Spain
|
| Modern SMT Solver Implementation
| Leonardo DeMoura & Nikolaj Bjorner | Microsoft Research, Redmond, USA
|
| Approaches to Parallel SAT Solving
| Youssef Hamadi
| Microsoft Research, Cambridge, UK
|
MaxSAT for Optimization Problems
| Joao Marques-Silva
| University College Dublin, Dublin, Ireland
|
| Non-DPLL Approaches to Boolean SAT Solving
| Bart Selman & Carla Gomes
| Cornell University, Ithaca, USA
|
| SMT-LIB Initiative
| Cesare Tinelli
| University of Iowa, Iowa City, USA
|
| Complexity Theoretic Aspects of the Boolean SAT Problem
| Ryan Williams
| IBM Almaden Research Center, San Jose, USA
|
Proof Complexity and Complexity of SAT Solvers
|
Sam Buss
|
University of California, San Diego, USA |
|
|
|
|
| Category 2: Description of SAT/SMT Solvers with tight focus on an application
|
| Cryptography and SAT Solvers -- Why and How
| Mate Soos
| Security Research Labs, Paris, France
|
| Yices and Applications
| Bruno Dutertre
| SRI International, Menlo Park, USA
|
| CVC3 and Applications
| Clark Barrett
| New York University, New York, USA
|
| SAT4J: pseudo-boolean optimization & dependency management problems
| Daniel LeBerre
| Université d'Artois, France
|
| SAT-based Model-Checking
|
Armin Biere
|
Johannes Kepler University, Linz, Austria
|
| SAT solving in AI
| Henry Kautz
| University of Rochester, Rochester, USA
|
Calculus of Data Structures for Verification and Synthesis
| Viktor Kuncak & Ruzica Piskac
| EPFL, Lausanne, Switzerland
|
| Alloy/Kodkod and Applications
| Emina Torlak
| LogicBlox, Atlanta, Georgia, USA
|
| HAMPI: A Solver for String Theories
| Vijay Ganesh
| MIT, Cambridge, USA
|
| OpenSMT and Applications
| R. Bruttomesso & N. Sharygina
| University of Lugano, Lugano, Switzerland
|
UCLID and Applications
|
Randy Bryant & Sanjit Seshia
|
CMU, Pittsburgh and UC, Berkeley, USA
|
| MathSAT and Applications |
Alessandro Cimatti
|
Fondazione Bruno Kessler, Trento, Italy
|
|
| Category 3: Description of tools using SAT/SMT Solvers
|
| Sketching: Program Synthesis using SAT Solvers
| Armando Solar-Lezama
| MIT, Cambridge, USA
|
| BitBlaze & WebBlaze: Tools for computer security using SMT Solvers
| Dawn Song & Prateek Saxena
| University of California, Berkeley, USA
|
SAGE: Automated Whitebox Fuzzing using SMT solvers
| Patrice Godefroid & David Molnar
| Microsoft Research, Redmond, USA
|
HAVOC: SMT solvers for precise and scalable reasoning of programs
| Shuvendu Lahiri & Shaz Qadeer
| Microsoft Research, Redmond, USA
|
| Liquid Types: SMT Solver-based Types
| Ranjit Jhala
| University of California, San Diego, USA
|
Scalable Testing/Reverse Engineering/Performance Profiling with Parallel and Selective Symbolic Execution
| George Candea & Stefan Bucur
| EPFL, Lausanne, Switzerland
|
|
Klee: An SMT Solver-based Dynamic Symbolic Testing Tool
| Cristian Cadar
| Imperial College London, London, UK
|
SAT-based Design Debugging
|
Sharad Malik
|
Princeton University, Princeton, USA
|
Harnessing SMT power using the verification engine Boogie
|
Rustan Leino
|
Microsoft Research, Redmond, USA
|
SMT Solver-based Compiler Optimization Verification
|
Sorin Lerner
|
University of California, San Diego, USA
|
CEGAR+SMT: Formal Verification of Control Logic in the Reveal System
|
Karem Sakallah
|
University of Michigan, Ann Arbor, USA |
| SAT Solvers for Formal Verification |
Ed Clarke
|
Carnegie Mellon University, Pittsburgh, USA |
| Symbolic Execution and Automated Exploit Generation |
David Brumley
|
Carnegie Mellon University, Pittsburgh, USA |
