...
Welcome
...
to
...
the
...
First
...
International
...
SAT/SMT
...
Summer
...
School
...
2011
Lectures Schedule
Time | Sunday 12 | Monday 13 | Tuesday 14 | Wed. 15 | Thursday 16 | Friday 17 |
|---|---|---|---|---|---|---|
08:30-09:30 |
...
...
...
...
...
...
...
...
...
...
...
...
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 |
|---|---|---|---|---|---|---|
10:00-11:00 |
...
...
...
...
...
...
...
...
...
...
Modern SMT Solver Implementation (Leonardo DeMoura & 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 | |
11:15-12:15 |
|---|
...
...
...
...
...
...
...
...
...
...
...
HAMPI: |
...
A |
...
Solver |
...
for |
...
String |
...
Theories |
...
(Vijay |
...
Ganesh) |
...
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 |
...
...
...
...
...
...
...
...
Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak) | SAT-based Model-Checking (Armin Biere) | Liquid Types: SMT Solver-based Types | Empirical Complexity (Holger Hoos) | ||
|---|---|---|---|---|---|
15:15-16:15 |
...
...
...
...
...
CVC3 and Applications (Clark |
...
Barrett) |
...
CryptoMiniSAT: |
...
A |
...
SAT |
...
Solver |
...
for |
...
Cryptography |
...
(Mate |
...
Soos) |
...
SAT4J: |
...
pseudo-boolean |
...
optimization |
...
& |
...
dependency |
...
management |
...
problems |
...
UCLID |
...
and |
...
Applications |
...
SMT |
...
Solver-based |
...
Compiler |
...
Optimization |
...
Verification |
16:15-16:45 |
|---|
...
Coffee |
...
break |
...
Coffee |
...
break |
...
Coffee |
...
break |
...
Coffee |
...
break |
...
Coffee |
...
break |
...
Coffee |
...
break |
16:45-17:45 |
|---|
...
...
...
...
...
...
...
CEGAR+SMT: |
...
Formal |
...
Verification |
...
of |
...
Control |
...
Logic |
...
in |
...
the |
...
Reveal |
...
System |
...
(Karem |
...
Sakallah) |
...
SAGE: |
...
Automated |
...
Whitebox |
...
Fuzzing |
...
using |
...
SMT |
...
solvers |
...
Parallelized |
...
Software |
...
Testing |
...
at |
...
Scale |
...
using |
...
SMT |
...
Solvers |
...
...
...
...
...
...
...
...
...
Non-DPLL |
...
Approaches |
...
to |
...
Boolean |
...
SAT |
...
Solving |
| Section | ||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
{section}
{column:width=60%}
{
|