Versions Compared

Old Version 46

changes.mady.by.user Unknown User (viganesh@mit.edu)

Saved on

compared with

New Version Current

changes.mady.by.user Unknown User (sseshia_1@touchstonenetwork.net)

Saved on

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

Sunday 12

Welcome coffee

Opening Remarks by Vijay Ganesh

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)

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

Time

Monday 13

Welcome to the First International SAT/SMT Summer School 2011

Lectures Schedule

00 45

Time

Sunday 12

Monday 13

Tuesday 14

Wed. 15

Thursday 16

Friday 17

08:30-09:30

Background Color
colorblue
The P vs. NP Question and Gödel's Lost Letter (Richard Lipton)
Independence Results for the P vs. NP Question (Shai Ben David)

Background Color
colororange
SAT Based Design Debugging
TBA
(Sharad Malik)

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

Background Color
coloryellow
Complexity Theoretic Aspects of the Boolean SAT Problem
SAT solving in AI (Henry Kautz)

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

09:30-10h00 :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

Coffee break

10 11:0015-11:00 12:30

Background Color
colorblue
Foundations of Modern CDCL SAT Solver Implementation (Niklas Een)
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)

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

Klee: An SMT Solver-based Dynamic Symbolic Testing Tool (Cristian Cadar)

HAMPI: A Solver for String Theories (Vijay Ganesh)

Yices and Applications

Alloy/Kodkod and Applications (Emina Torlak)

OpenSMT and Applications

MathSAT and Applications

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 12:15-14:00

Lunch

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 Solvers for Formal Verification (Ed Clarke)

Calculus of Data Structures for Verification and Synthesis (Viktor Kuncak)

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
Empirical Complexity (Holger Hoos
(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
SMT-LIB Initiative (Cesare Tinelli)
CVC3 and Applications (Clark Barrett)

Background Color
coloryellow
CryptoMiniSat -- A Rough Guide
CryptoMiniSAT: A SAT Solver for Cryptography
(Mate Soos)

Background Color
coloryellow
SAT4J: pseudo-boolean optimization & dependency management problems

UCLID and Applications

(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

Coffee break

16:45-17h45/18:00

17:

00-18:00

Background Color
colororange
SMT Theory and DPLL(T) (Albert Oliveras)
CEGAR+SMT: Formal Verification of Control Logic in the Reveal System (Karem Sakallah)

Background Color
colororange
SAGE: Automated Whitebox Fuzzing using SMT solvers

Parallelized Software Testing at Scale using SMT Solvers

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

(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)
Non-DPLL Approaches to Boolean SAT Solving

Class Website on MIT Stellar Course Site

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