...
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) | 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) | BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena) | 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 |
| Klee: An SMT Solver-based Dynamic Symbolic Testing Tool |
| HAMPI: A Solver for String Theories (Vijay Ganesh) | Yices and Applications | Alloy/Kodkod and Applications (Emina Torlak) | OpenSMT and Applications | MathSAT and Applications |
12:15-14:00 | Lunch | |||||||
14:00-15:00 | Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak) | SAT-based Model-Checking (Armin Biere) | Liquid Types: SMT Solver-based Types | Empirical Complexity (Holger Hoos) | ||||
15:15-16:15 | CVC3 and Applications (Clark Barrett) | CryptoMiniSAT: A SAT Solver for Cryptography (Mate Soos) | 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 | 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 | Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)\ | Non-DPLL Approaches to Boolean SAT Solving |
...