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

|| Legend | {bgcolor:blue}Category 1: Foundational Aspects of SAT/SMT Solvers {bgcolor}| {bgcolor:yellow}Category 2: Description of SAT/SMT Solvers with tight focus on an application {bgcolor}| {bgcolor:orange}Category 3: Description of tools using SAT/SMT Solvers{bgcolor} |

Each lecture lasts one hour for single speaker, and one hour fifteen minutes for two speakers.
h2. Sunday, May 12, specific schedule

|| Time || 08:30-08:45 || 08-45:09:45 || 09:45-10:15 || 10:15-11:15 || 11:30-12:30 || 12:30-14:00 || 14:00-15:00 || 15:15-16:15 || 16:15-16:45 || 16:45-17:45 ||
|| Sunday 12 || Opening (Vijay Ganesh) | {bgcolor:blue}[The P vs. NP Question and Gödel's Lost Letter (Richard Lipton)|PvsNP]
 {bgcolor} || Coffee break | {bgcolor:blue}[Foundations of Modern CDCL SAT Solver Implementation (Niklas Een)|FoundationsSat] {bgcolor} | {bgcolor:orange}[Klee: An SMT Solver-based Dynamic Symbolic Testing Tool (Cristian Cadar)|Klee] {bgcolor} || Lunch | {bgcolor:orange}[SAT Solvers for Formal Verification (Ed Clarke)|SatFormalVerification] {bgcolor} | {bgcolor:blue}[SMT-LIB Initiative (Cesare Tinelli)|SmtLib] {bgcolor} || Coffee break | {bgcolor:blue}[SMT Theory and DPLL(T) (Albert Oliveras)|FoundationsSmt] {bgcolor} ||

h2. May 13-17, regular schedule

|| Time || Monday 13 || Tuesday 14 || Wed. 15 || Thursday 16 || Friday 17 ||
|| 08:30-09:30 | {bgcolor:blue}[Independence Results for the P vs. NP Question (Shai Ben David)|Independence] {bgcolor} | {bgcolor:orange}TBA (Sharad Malik) {bgcolor} | {bgcolor:blue}[Complexity Theoretic Aspects of the Boolean SAT Problem (Ryan Williams)|TheoreticAspectsSat] {bgcolor} | {bgcolor:yellow}[SAT solving in AI (Henry Kautz)|SatAI] {bgcolor} | {bgcolor:blue}[Proof Complexity and Complexity of SAT Solvers (Sam Buss)|ProofComplexitySat]
 {bgcolor} ||
|| 09:30-10:00 || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break ||
|| 10:00-11:00 | {bgcolor:yellow}[HAMPI: A Solver for String Theories (Vijay Ganesh)|Hampi] {bgcolor} |{bgcolor:yellow}[Yices and Applications (Bruno Dutertre)|Yices] {bgcolor}| {bgcolor:blue}[Approaches to Parallel SAT Solving (Youssef Hamadi)|ParallelSat]
 {bgcolor} | {bgcolor:orange}[HAVOCSketching: SMTProgram solversSynthesis forusing precise and scalable reasoning of programsSAT Solvers (Shuvendu Lahiri & Shaz QadeerArmando Solar-Lezama)|HavocSketching]
 {bgcolor}  | {bgcolor:orange}[Harnessing SMT power using the verification engine Boogie (Rustan Leino)|Boogie] {bgcolor} ||
|| 11:15-12:15/12:30 | {bgcolor:blue}[Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)|ModernSMT] {bgcolor} | {bgcolor:orange}[BitBlaze & WebBlaze: Tools for computer security using SMT Solvers  (Dawn Song & Prateek Saxena)|WebBlaze]
 {bgcolor} | {bgcolor:yellow}[Alloy/Kodkod and Applications (Emina Torlak)|Kodkod]\\ \\
 {bgcolor} | {bgcolor:orange}[Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)|Sketching]HAVOC: SMT solvers for precise and scalable reasoning of programs (Shuvendu Lahiri & Shaz Qadeer)|Havoc]
 {bgcolor}  | {bgcolor:yellow}[MathSAT and Applications (Roberto Sebastiani & Alessandro Cimatti)|MathSat]\\ \\
 {bgcolor}||
|| 12:15/12-30-14:00 || Lunch || Lunch || Lunch || Lunch || Lunch ||
|| 14:00-15:00 | {bgcolor:yellow}[Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak)|CalculusDataStructure] {bgcolor} | {bgcolor:yellow}[SAT-based Model-Checking (Armin Biere)|ModelChecking]
 {bgcolor} | {bgcolor:blue}[MaxSAT for Optimization Problems (Joao Marques-Silva)|MaxSAT] {bgcolor} | {bgcolor:orange}[Liquid Types: SMT Solver-based Types (Ranjit Jhala)|LiquidTypes] {bgcolor} | {bgcolor:blue}[Empirical Complexity (Holger Hoos)|EmpiricalComplexity] {bgcolor} ||
|| 15:15-16:15 | {bgcolor:yellow}[CVC3 and Applications (Clark Barrett)|Cvc3]{bgcolor} | {bgcolor:yellow}[CryptoMiniSAT: A SAT Solver for Cryptography (Mate Soos)|Cryptominisat]{bgcolor} | {bgcolor:yellow}[SAT4J: pseudo-boolean optimization & dependency management problems (Daniel Le Berre)|Sat4j]{bgcolor} | {bgcolor:yellow}[UCLID and Applications (Randy Bryant & Sanjit Seshia)|Uclid]\\
 {bgcolor} | {bgcolor:orange}[SMT Solver-based Compiler Optimization Verification (Sorin Lerner)|CompilerOptimizationVerification]{bgcolor} ||
|| 16:15-16:45 || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break ||
|| 16:45-17h45/18:00 | {bgcolor:orange}[CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)|CegarSmt] {bgcolor} | {bgcolor:orange}[SAGE: Automated Whitebox Fuzzing using SMT solvers (Patrice Godefroid & David Molnar)|Sage] \\ \\ \\{bgcolor} | {bgcolor:orange}[Parallelized Software Testing at Scale using SMT Solvers (Stefan Bucur & George Candea)|ParallelizedSoftwareTestingSmt] \\ \\ \\{bgcolor} | {bgcolor:yellow}[OpenSMT and Applications (Roberto Bruttomesso & Natasha Sharygina)|OpenSMT]
 \\ \\ \\ \\{bgcolor} | {bgcolor:blue}[Non-DPLL Approaches to Boolean SAT Solving (Bart Selman & Carla Gomes)|NonDpll] \\ \\{bgcolor} ||

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