Lectures Schedule

Legend

Category 1: Foundational Aspects of SAT/SMT Solvers

Category 2: Description of SAT/SMT Solvers with tight focus on an application

Category 3: Description of tools using SAT/SMT Solvers

Each lecture lasts one hour (1:00) for single speaker, and one hour fifteen minutes (1:15) for dual speakers.

Sunday, June 12, special schedule

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

Introduction to Satisfiability Solving with Practical Applications (Niklas Een)

Coffee break

SMT Theory and DPLL(T) (Albert Oliveras)

Lunch

SAT Solvers for Formal Verification (Ed Clarke)

SMT-LIB Initiative (Cesare Tinelli)

Coffee break

Constraint Solving Challenges in Dynamic Symbolic Execution (Cristian Cadar)

Monday, June 13 to Friday, June 17, regular schedule

Time	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)	SAT Based Design Debugging (Sharad Malik)	Calculus of Data Structures for Verification & Synthesis (Ruzica Piskac)	SAT solving in AI (Henry Kautz)	Proof Complexity and Complexity of SAT Solvers (Sam Buss)
09:45-10:45	HAMPI: A Solver for String Theories (Vijay Ganesh)	Yices and Applications (Bruno Dutertre)	Approaches to Parallel SAT Solving (Youssef Hamadi)	Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)	Harnessing SMT power using the verification engine Boogie (Rustan Leino)
10:45-11:15	Coffee break	Coffee break	Coffee break	Coffee break	Coffee break
11:15-12:30	Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)	BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena)	UCLID's Elements: Term-Level Verification and SMT Solving (Randy Bryant & Sanjit Seshia)	MathSAT and Applications (Alessandro Cimatti)	HAVOC: SMT solvers for precise and scalable reasoning of programs (Shuvendu Lahiri & Shaz Qadeer)
12-30-14:00	Lunch	Lunch	Lunch	Lunch	Lunch
14:00-15:00	14:00-15:15 Parallel and Selective Symbolic Execution (George Candea & Stefan Bucur)	SAT-based Model-Checking (Armin Biere)	MaxSAT for Optimization Problems (Joao Marques-Silva)	Liquid Types: SMT Solver-based Types (Ranjit Jhala)	Non-DPLL Approaches to Boolean SAT Solving (Bart Selman & Carla Gomes)
15:15-16:15	15:30-16:30 CVC3 and Applications (Clark Barrett)	CryptoMiniSat -- A Rough Guide (Mate Soos)	SAT4J: pseudo-boolean optimization & dependency management problems (Daniel Le Berre)	Alloy/Kodkod and Applications (Emina Torlak)	SMT Solver-based Compiler Optimization Verification (Sorin Lerner)
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 CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)	SAGE: Automated Whitebox Fuzzing using SMT solvers (Patrice Godefroid & David Molnar)	SAT Solving and Complexity Theory (Ryan Williams)	OpenSMT and Applications (Roberto Bruttomesso & Natasha Sharygina)	Symbolic Execution and Automated Exploit Generation (David Brumley)

Class Website on MIT Stellar Course Site

UCLID's Elements: Term-Level Verification and SMT Solving

Child pages

SATSMT Summer School 2011

Lectures Schedule

Sunday, June 12, special schedule

Monday, June 13 to Friday, June 17, regular schedule

Class Website on MIT Stellar Course Site

UCLID's Elements: Term-Level Verification and SMT Solving