Lectures Schedule

Legend

This page contains macros or features from a plugin which requires a valid license.

You will need to contact your administrator.

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

  • No labels