...
Time | Sunday 12 | Monday 13 | Tuesday 14 | Wed. 15 | Thursday 16 | Friday 17 | |
|---|---|---|---|---|---|---|---|
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) |
| Complexity Theoretic Aspects of the Boolean SAT Problem |
| 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) |
| Approaches to Parallel SAT Solving (Youssef Hamadi) |
|
| |
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) |
|
|
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 |
| 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 |
|
| |
16:15-16:45 | Coffee break | ||||||
16:45-17:45 | SMT Theory and DPLL(T) (Albert Oliveras) Non-DPLL Approaches to Boolean SAT Solving | CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah) |
| SAT solving in AI |
| Non-DPLL Approaches to Boolean SAT Solving |
| Section | ||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|