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

{bgcolor:blue}Category 1: Foundational Aspects of

Legend

Background Color
colorblue
Category 1: Foundational Aspects of

Wiki Markup
SAT/SMT

Solvers

{

Background Color

}

coloryellow
Category 2: Description of

Wiki Markup{bgcolor:yellow}Category 2: Description of

SAT/SMT

Solvers

with

tight

focus

on

an

application

{

Background Color

}

colororange
Category 3: Description of tools using

Wiki Markup{bgcolor:orange}Category 3: Description of tools using

SAT/SMT

Solvers

{bgcolor}

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

...

{bgcolor:orange}[Constraint Solving Challenges in Dynamic Symbolic Execution (Cristian Cadar)|Klee] {bgcolor}

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

Background Color
colorblue
Introduction to Satisfiability Solving with Practical Applications (Niklas Een)

Coffee break

Background Color
colorblue
SMT Theory and DPLL(T) (Albert Oliveras)

Lunch

Background Color
colororange
SAT Solvers for Formal Verification (Ed Clarke)

Background Color
colorblue
SMT-LIB Initiative (Cesare Tinelli)

Coffee break

Background Color
colororange
Constraint Solving Challenges in Dynamic Symbolic Execution (Cristian Cadar)

Wiki Markup

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

{bgcolor:blue}[Proof Complexity and Complexity of SAT Solvers (Sam Buss)|ProofComplexitySat] {bgcolor}

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}

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)

Wiki Markup

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}

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)

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}

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)

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}

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)

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}

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)

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

Background Color
colororange
Wiki Markup
{bgcolor:orange}[CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)|CegarSmt] {

}
Background Color

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}

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)

Wiki Markup{bgcolor:orange}[Symbolic Execution and Automated Exploit Generation (David Brumley)|SymbolicExploitGeneration] {bgcolor}

Class Website on MIT Stellar Course Site

...