08:30-09:30

The P vs. NP Question and Gödel's Lost Letter (Richard Lipton)

Independence Results for the P vs. NP Question (Shai Ben David)

TBA (Sharad Malik)

Complexity Theoretic Aspects of the Boolean SAT Problem

SAT solving in AI (Henry Kautz)

Proof Complexity and Complexity of SAT Solvers

09:30-10h00

Coffee break

10:00-11:00

Foundations of Modern CDCL SAT Solver Implementation (Niklas Een)

Modern SMT Solver Implementation (Leonardo DeMoura & Nikolaj Bjorner)

HAMPI: A Solver for String Theories (Vijay Ganesh)

Approaches to Parallel SAT Solving (Youssef Hamadi)

HAVOC: SMT solvers for precise and scalable reasoning of programs

Harnessing SMT power using the verification engine Boogie

11:15-12:15

Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)

BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena)

Yices and Applications

Alloy/Kodkod and Applications (Emina Torlak)

OpenSMT and Applications

MathSAT and Applications

12:15-14:00

Lunch

14:00-15:00

SAT Solvers for Formal Verification (Ed Clarke)

Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak)

SAT-based Model-Checking (Armin Biere)

MaxSAT for Optimization Problems

Liquid Types: SMT Solver-based Types

Empirical Complexity (Holger Hoos)

15:15-16:15

SMT-LIB Initiative (Cesare Tinelli)

CryptoMiniSAT: A SAT Solver for Cryptography (Mate Soos)

CVC3 and Applications

SAT4J: pseudo-boolean optimization & dependency management problems

UCLID and Applications

SMT Solver-based Compiler Optimization Verification

16:15-16:45

Coffee break

16:45-17:45

SMT Theory and DPLL(T) (Albert Oliveras)

CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)

SAGE: Automated Whitebox Fuzzing using SMT solvers

Parallelized Software Testing at Scale using SMT Solvers

Klee: An SMT Solver-based Dynamic Symbolic Testing Tool

Non-DPLL Approaches to Boolean SAT Solving