| Wiki Markup |
|---|
h1. Welcome to the {color:#0000ff}{*}+[First International SAT/SMT Summer School |
...
Lectures Schedule
...
Time
...
Sunday 12
...
Monday 13
...
Tuesday 14
...
Wed. 15
...
Thursday 16
...
Friday 17
2011|http://people.csail.mit.edu.ezproxyberklee.flo.org/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) |
...
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
...
Coffee break
...
Coffee break
...
Coffee break
...
Coffee break
...
Coffee break
|PvsNP]{bgcolor}| [Independence Results for the P vs. NP Question (Shai Ben David)|Independence] | 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 || Coffee break || Coffee break || Coffee break || Coffee break || Coffee break || || 10:00-11:00 |
...
| [Foundations of Modern CDCL SAT Solver Implementation (Niklas Een) |
...
Modern SMT Solver Implementation (Leonardo De Moura& 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
|FoundationsSat] | [Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)|ModernSMT] | 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 (Cristian Cadar) |
...
|Klee] | [HAMPI: A Solver for String Theories (Vijay Ganesh) |
...
Yices and Applications
|Hampi] | 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
|| Lunch || Lunch || Lunch || Lunch || Lunch || 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 (Joao Marques-Silva)
...
Liquid Types: SMT Solver-based Types
...
Empirical Complexity (Holger Hoos)
|SatFormalVerification] | [Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak)|CalculusDataStructure] \\ | 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 |
...
| [SMT-LIB Initiative (Cesare Tinelli) |
...
|SmtLib] | [CVC3 and Applications (Clark Barrett) |
...
|Cvc3] | [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 |
...
| [SMT Theory and DPLL(T) (Albert Oliveras) |
...
|FoundationsSmt] | [CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah) |
...
|CegarSmt] \\ | [SAGE: Automated Whitebox Fuzzing using SMT |
...
Parallelized Software Testing at Scale using SMT Solvers
...
Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)
...
Non-DPLL Approaches to Boolean SAT Solving
...
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://mv.ezproxy.com.ezproxyberklee.flo.org/S/project/satsmtschool11/]{color} |