Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migration of unmigrated content due to installation of a new plugin

Lectures Schedule

Legend

Background Color
colorblue
Category 1: Foundational Aspects of SAT/SMT Solvers

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

Background Color
colororange
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

...

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

Time

Monday 13

Tuesday 14

Wed. 15

Thursday 16

Friday 17

08:30-09:30

...

Background Color
colorblue
Independence Results for the P vs. NP Question (Shai Ben David)

Background Color
colororange
SAT Based Design Debugging (Sharad Malik)

Background Color
coloryellow
Calculus of Data Structures for Verification & Synthesis (Ruzica Piskac)

Background Color
coloryellow
SAT solving in AI (Henry Kautz)

Background Color
colorblue
Proof Complexity and Complexity of SAT Solvers (Sam Buss)

09:45-10:45

Background Color
coloryellow
HAMPI: A Solver for String Theories (Vijay Ganesh)

Background Color
coloryellow
Yices and Applications (Bruno Dutertre)

Background Color
colorblue
Approaches to Parallel SAT Solving (Youssef Hamadi)

Background Color
colororange
Sketching: Program Synthesis using SAT Solvers (Armando Solar-Lezama)

Background Color
colororange
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

Background Color
colorblue
Modern SMT Solver Implementation (Leonardo De Moura& Nikolaj Bjorner)

Background Color
colororange
BitBlaze & WebBlaze: Tools for computer security using SMT Solvers (Dawn Song & Prateek Saxena)

Background Color
coloryellow
UCLID's Elements: Term-Level Verification and SMT Solving (Randy Bryant & Sanjit Seshia)

Background Color
coloryellow
MathSAT and Applications (Alessandro Cimatti)

Background Color
colororange
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

Background Color
colororange
Parallel and Selective Symbolic Execution (George Candea & Stefan Bucur)

Background Color
coloryellow
SAT-based Model-Checking (Armin Biere)

Background Color
colorblue
MaxSAT for Optimization Problems (Joao Marques-Silva)

Background Color
colororange
Liquid Types: SMT Solver-based Types (Ranjit Jhala)

Background Color
colorblue
Non-DPLL Approaches to Boolean SAT Solving (Bart Selman & Carla Gomes)

15:15-16:15

15:30-16:30

Background Color
coloryellow
CVC3 and Applications (Clark Barrett)

Background Color
coloryellow
CryptoMiniSat -- A Rough Guide (Mate Soos)

Background Color
coloryellow
SAT4J: pseudo-boolean optimization & dependency management problems (Daniel Le Berre)

Background Color
coloryellow
Alloy/Kodkod and Applications (Emina Torlak)

Background Color
colororange
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

Background Color
colororange
CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)

Background Color
colororange
SAGE: Automated Whitebox Fuzzing using SMT solvers (Patrice Godefroid & David Molnar)

Background Color
colorblue
SAT Solving and Complexity Theory (Ryan Williams)

Background Color
coloryellow
OpenSMT and Applications (Roberto Bruttomesso & Natasha Sharygina)

Background Color
colororange
Symbolic Execution and Automated Exploit Generation (David Brumley)

Class Website on MIT Stellar Course Site

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