Page History

h1. Welcome to the {color:#0000ff}{*}+[First International SAT/SMT Summer School 2011|http://people.csail.mit.edu/vganesh/summerschool]+{*}{color}


h1. Lectures Schedule

|| Time || Sunday 12 || Monday 13 || Tuesday 14 || Wed. 15 || Thursday 16 || Friday 17 ||
|| 08:30-09:30 | {bgcolor:blue}[The P vs. NP Question and Gödel's Lost Letter (Richard Lipton)|PvsNP]{bgcolor} | {bgcolor:blue}[Independence Results for the P vs. NP Question (Shai Ben David)|Independence] {bgcolor} | TBA (Sharad Malik) | {bgcolor:blue}Complexity Theoretic Aspects of the Boolean SAT Problem {bgcolor} | SAT solving in AI (Henry Kautz) | {bgcolor:blue}Proof Complexity and Complexity of SAT Solvers {bgcolor} ||
|| 09:30-10h00 || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break ||
|| 10:00-11:00 | {bgcolor:blue}[Foundations of Modern CDCL SAT Solver Implementation (Niklas Een)|FoundationsSat] {bgcolor} | {bgcolor:blue}[Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)|ModernSMT] {bgcolor} | 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 | {bgcolor:yellow}[Klee: An SMT Solver-based Dynamic Symbolic Testing Tool (Cristian Cadar)|Klee] {bgcolor} | {bgcolor:yellow}[HAMPI: A Solver for String Theories (Vijay Ganesh)|Hampi] {bgcolor} | Yices and Applications | Alloy/Kodkod and Applications (Emina Torlak) | OpenSMT and Applications | MathSAT and Applications ||
|| 12:15-14:00 || Lunch || Lunch || Lunch || Lunch || Lunch || Lunch ||
|| 14:00-15:00 | {bgcolor:orange}[SAT Solvers for Formal Verification (Ed Clarke)|SatFormalVerification] {bgcolor} | {bgcolor}[Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak)|CalculusDataStructure]{bgcolor:yellow} | SAT-based Model-Checking (Armin Biere) | [MaxSAT for Optimization Problems (Joao Marques-Silva)|MaxSAT] | Liquid Types: SMT Solver-based Types \| Empirical Complexity (Holger Hoos) \\ ||
|| 15:15-16:15 | {bgcolor:blue}[SMT-LIB Initiative (Cesare Tinelli)|SmtLib] ||{bgcolor} | {bgcolor:yellow}[CVC3 and Applications (Clark Barrett)|Cvc3]{bgcolor} | [CryptoMiniSAT: A SAT Solver for Cryptography (Mate Soos)|Cryptominisat] \\ | [SAT4J: pseudo-boolean optimization & dependency management problems|Sat4j] | [UCLID and Applications|Uclid] | [SMT Solver-based Compiler Optimization Verification |CompilerOptimizationVerification] ||
|| 16:15-16:45 || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break ||
|| 16:45-17:45 | {bgcolor:blue}[SMT Theory and DPLL(T) (Albert Oliveras)|FoundationsSmt] {bgcolor} | {bgcolor:orange}[CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)|CegarSmt] {bgcolor} | [SAGE: Automated Whitebox Fuzzing using SMT solvers|Sage] | [Parallelized Software Testing at Scale using SMT Solvers|ParallelizedSoftwareTestingSmt] | [Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)|Sketching] | [Non-DPLL Approaches to Boolean SAT Solving|NonDpll] ||

h1. {color:#0000ff}[Class Website on MIT Stellar Course Site|http://stellar.mit.edu/S/project/satsmtschool11/]{color}