Lectures Schedule
Legend | | Background Color |
|---|
| | Category 1: Foundational Aspects of |
| Wiki Markup |
|---|
{bgcolor:blue}Category 1: Foundational Aspects of { | } |
|---|
| | Category 2: Description of |
| Wiki Markup |
|---|
{bgcolor:yellow}Category 2: Description of { | } |
|---|
| | Category 3: Description of tools using |
| Wiki Markup |
|---|
{bgcolor:orange}Category 3: Description of tools using {bgcolor} |
|---|
Each lecture lasts one hour (1:00) for single speaker, and one hour fifteen minutes (1:15) for dual speakers.
...
Time | 08:30-09:30 | 09:30-10:00 | 10:00-11:00 | 11:00-11:30 | 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 | Welcome coffee | Opening Remarks by Vijay Ganesh | | Wiki Markup |
|---|
{bgcolor:blue}[Introduction to Satisfiability Solving with Practical Applications (Niklas Een)|FoundationsSat] {bgcolor} |
| Coffee break | | Wiki Markup |
|---|
{bgcolor:blue}[SMT Theory and DPLL(T) (Albert Oliveras)|FoundationsSmt] {bgcolor} |
| Lunch | | Wiki Markup |
|---|
{bgcolor:orange}[SAT Solvers for Formal Verification (Ed Clarke)|SatFormalVerification] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:blue}[SMT-LIB Initiative (Cesare Tinelli)|SmtLib] {bgcolor} |
| Coffee break | | | Coffee break | | Lunch | | | Coffee break | | Wiki Markup |
|---|
{bgcolor:orange}[Constraint Solving Challenges in Dynamic Symbolic Execution (Cristian Cadar)|Klee] {bgcolor} |
|---|
Monday, June 13 to Friday, June 17, regular schedule
Time | Monday 13 | Tuesday 14 | Wed. 15 | Thursday 16 | Friday 17 |
|---|
08:30-09:30 | | Wiki Markup |
|---|
{bgcolor:blue}[Independence Results for the P vs. NP Question (Shai Ben David)|Independence] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:orange}[SAT Based Design Debugging (Sharad Malik)|SatDesignDebugging] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[Calculus of Data Structures for Verification & Synthesis (Ruzica Piskac)|CalculusDataStructure] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[SAT solving in AI (Henry Kautz)|SatAI] {bgcolor} |
| | | | | | Wiki Markup |
|---|
{bgcolor:blue}[Proof Complexity and Complexity of SAT Solvers (Sam Buss)|ProofComplexitySat] {bgcolor} |
|---|
09:45-10:45 | | Wiki Markup |
|---|
{bgcolor:yellow}[HAMPI: A Solver for String Theories (Vijay Ganesh)|Hampi] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[Yices and Applications (Bruno Dutertre)|Yices] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:blue}[Approaches to Parallel SAT Solving (Youssef Hamadi)|ParallelSat] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:orange}[Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)|Sketching] {bgcolor} |
| | | | | | Wiki Markup |
|---|
{bgcolor:orange}[Harnessing SMT power using the verification engine Boogie (Rustan Leino)|Boogie] {bgcolor} |
|---|
10:45-11:15 | Coffee break | Coffee break | Coffee break | Coffee break | Coffee break |
|---|
11:15-12:30 | | Wiki Markup |
|---|
{bgcolor:blue}[Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)|ModernSMT] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:orange}[BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena)|WebBlaze] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[UCLID's Elements: Term-Level Verification and SMT Solving (Randy Bryant & Sanjit Seshia)|Uclid] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[MathSAT and Applications (Alessandro Cimatti)|MathSat] {bgcolor} |
| | | | | | | Wiki Markup |
|---|
{bgcolor:orange}[HAVOC: SMT solvers for precise and scalable reasoning of programs (Shuvendu Lahiri & Shaz Qadeer)|Havoc] {bgcolor} |
|---|
12-30-14:00 | Lunch | Lunch | Lunch | Lunch | Lunch |
|---|
14:00-15:00 | 14:00-15:15 | Wiki Markup |
|---|
{bgcolor:orange}[Parallel and Selective Symbolic Execution (George Candea & Stefan Bucur)|Parallel & Selective Symbolic Execution] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[SAT-based Model-Checking (Armin Biere)|ModelChecking] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:blue}[MaxSAT for Optimization Problems (Joao Marques-Silva)|MaxSAT] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:orange}[Liquid Types: SMT Solver-based Types (Ranjit Jhala)|LiquidTypes] {bgcolor} |
| | | | | | Wiki Markup |
|---|
{bgcolor:blue}[Non-DPLL Approaches to Boolean SAT Solving (Bart Selman & Carla Gomes)|NonDpll] {bgcolor} |
|---|
15:15-16:15 | 15:30-16:30 | Wiki Markup |
|---|
|
|---|
{bgcolor:yellow}[CVC3 and Applications (Clark Barrett)|Cvc3] {bgcolor} |
| Wiki Markup |
|---|
{bgcolor:yellow}[CryptoMiniSat \-\- A Rough Guide (Mate Soos)|Cryptominisat] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[SAT4J: pseudo-boolean optimization & dependency management problems (Daniel Le Berre)|Sat4j] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[Alloy/Kodkod and Applications (Emina Torlak)|Kodkod] {bgcolor} |
| | | | | | Wiki Markup |
|---|
{bgcolor:orange}[SMT Solver-based Compiler Optimization Verification (Sorin Lerner)|CompilerOptimizationVerification] {bgcolor} | 16:15-16:45 | 16:30-17:00
Coffee break | Coffee break | Coffee break | Coffee break | Coffee break |
|---|
16:45-17h45/18:00 | 17:00-18:00 | | | Wiki Markup |
|---|
{bgcolor:orange}[SAGE: Automated Whitebox Fuzzing using SMT solvers (Patrice Godefroid & David Molnar)|Sage] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:blue}[SAT Solving and Complexity Theory (Ryan Williams)|TheoreticAspectsSat] {bgcolor} |
| | Wiki Markup |
|---|
{bgcolor:yellow}[OpenSMT and Applications (Roberto Bruttomesso & Natasha Sharygina)|OpenSMT] {bgcolor} |
| | | | | Wiki Markup |
|---|
{bgcolor:orange}[Symbolic Execution and Automated Exploit Generation (David Brumley)|SymbolicExploitGeneration] {bgcolor} |
|---|
...