You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 35 Next »

Welcome to the First International SAT/SMT Summer School 2011

Class Website on MIT Stellar Course Site

Lectures Schedule

Time

Sunday 12

Monday 13

Tuesday 14

Wed. 15

Thursday 16

Friday 17

08:30-09:30

The P vs. NP Question and Gödel's Lost Letter (Richard Lipton)

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

TBA (Sharad Malik)

Complexity Theoretic Aspects of the Boolean SAT Problem

SAT solving in AI (Henry Kautz)

Proof Complexity and Complexity of SAT Solvers

09:30-10h00

Coffee break

Coffee break

Coffee break

Coffee break

Coffee break

Coffee break

10:00-11:00

Foundations of Modern CDCL SAT Solver Implementation (Niklas Een)

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

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

12:15-14:00

Lunch

Lunch

Lunch

Lunch

Lunch

Lunch

14:00-15:00

SAT Solvers for Formal Verification (Ed Clarke)

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

SAT-based Model-Checking (Armin Biere)

MaxSAT for Optimization Problems (Joao Marques-Silva)

Liquid Types: SMT Solver-based Types

Empirical Complexity (Holger Hoos)

15:15-16:15

SMT-LIB Initiative (Cesare Tinelli)

CVC3 and Applications (Clark Barrett)

CryptoMiniSAT: A SAT Solver for Cryptography (Mate Soos)

SAT4J: pseudo-boolean optimization & dependency management problems

UCLID and Applications

SMT Solver-based Compiler Optimization Verification

16:15-16:45

Coffee break

Coffee break

Coffee break

Coffee break

Coffee break

Coffee break

16:45-17:45

SMT Theory and DPLL(T) (Albert Oliveras)

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

SAGE: Automated Whitebox Fuzzing using SMT solvers

Parallelized Software Testing at Scale using SMT Solvers

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

Non-DPLL Approaches to Boolean SAT Solving

Recently Updated

Navigate space
  • No labels