First International SAT/SMT Summer School 2011
">Welcome to the First International SAT/SMT Summer School 2011
Lectures Schedule
Legend |
Unknown macro: {bgcolor} Category 1: Foundational Aspects of SAT/SMT Solvers |
Unknown macro: {bgcolor} Category 2: Description of SAT/SMT Solvers with tight focus on an application |
Unknown macro: {bgcolor} Category 3: Description of tools using SAT/SMT Solvers |
|---|
Each lecture lasts one hour for single speaker, and one hour fifteen minutes for two speakers.
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) |
Unknown macro: {bgcolor} The P vs. NP Question and Gödel's Lost Letter (Richard Lipton) |
Coffee break |
Unknown macro: {bgcolor} Foundations of Modern CDCL SAT Solver Implementation (Niklas Een) |
Unknown macro: {bgcolor} Klee: An SMT Solver-based Dynamic Symbolic Testing Tool (Cristian Cadar) |
Lunch |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor} |
Coffee break |
Unknown macro: {bgcolor} |
May 13-17, regular schedule
Time |
Monday 13 |
Tuesday 14 |
Wed. 15 |
Thursday 16 |
Friday 17 |
|---|---|---|---|---|---|
08:30-09:30 |
Unknown macro: {bgcolor} Independence Results for the P vs. NP Question (Shai Ben David) |
Unknown macro: {bgcolor} TBA (Sharad Malik) |
Unknown macro: {bgcolor} Complexity Theoretic Aspects of the Boolean SAT Problem (Ryan Williams) |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor}
|
09:30-10:00 |
Coffee break |
Coffee break |
Coffee break |
Coffee break |
Coffee break |
10:00-11:00 |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor}
|
Unknown macro: {bgcolor} HAVOC: SMT solvers for precise and scalable reasoning of programs (Shuvendu Lahiri & Shaz Qadeer) |
Unknown macro: {bgcolor} Harnessing SMT power using the verification engine Boogie (Rustan Leino) |
11:15-12:15/12:30 |
Unknown macro: {bgcolor} Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner) |
Unknown macro: {bgcolor} BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena) |
Unknown macro: {bgcolor}
|
Unknown macro: {bgcolor} Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama) |
Unknown macro: {bgcolor} MathSAT and Applications (Roberto Sebastiani & Alessandro Cimatti) |
12:15/12-30-14:00 |
Lunch |
Lunch |
Lunch |
Lunch |
Lunch |
14:00-15:00 |
Unknown macro: {bgcolor} Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak) |
Unknown macro: {bgcolor}
|
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor} |
15:15-16:15 |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor} |
Unknown macro: {bgcolor} SAT4J: pseudo-boolean optimization & dependency management problems (Daniel Le Berre) |
Unknown macro: {bgcolor}
|
Unknown macro: {bgcolor} SMT Solver-based Compiler Optimization Verification (Sorin Lerner) |
16:15-16:45 |
Coffee break |
Coffee break |
Coffee break |
Coffee break |
Coffee break |
16:45-17h45/18:00 |
Unknown macro: {bgcolor} CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah) |
Unknown macro: {bgcolor} SAGE: Automated Whitebox Fuzzing using SMT solvers (Patrice Godefroid & David Molnar) |
Unknown macro: {bgcolor} [Parallelized Software Testing at Scale using SMT Solvers (Stefan Bucur & George Candea)] |
Unknown macro: {bgcolor} OpenSMT and Applications (Roberto Bruttomesso & Natasha Sharygina)
|
Unknown macro: {bgcolor} Non-DPLL Approaches to Boolean SAT Solving (Bart Selman & Carla Gomes) |