Sunday, June 12- Friday, June 17, 2011

MIT Building 34 (Room 101), 50 Vassar Street, CAMBRIDGE, MA, USA


    Sponsored By


Microsoft Research

MIT Lincoln Laboratory
MIT Lincoln Laboratory


Reservoir Labs


Boolean SAT/SMT constraint solvers have seen dramatic progress in the last decade, and are being used in a diverse set of applications such as program analysis, testing, formal methods, program synthesis, hardware verification, electronic design automation, computer security, AI, operations research (MAXSAT) and biology.

It is with the goal of connecting SAT/SMT developers and power users that we have decided to organize the First International SAT/SMT Summer School from Sunday June 12th to Friday June 17th, 2011 at Building 34 (room 101 on the first floor), Massachusetts Institute of Technology, Cambridge, MA, USA.

Goals of the Summer School

  • To be a marketplace of ideas for SAT/SMT solver developers and power users
  • Connect new and current power users with SAT/SMT developers
  • Connect complexity theorists with SAT/SMT developers
  • Connect researchers in non-CDCL approaches (e.g., Physics inspired)  with researchers in CDCL-based approaches to SAT
  • Encourage discussion on solvers for multicores,  solver-based programming languages, and empirical complexity
The Lecturers

Following is the list of lectures and lecturers. Each lecture will be 1 hour long.

Lecture Title Lecturer Affiliation

Category 1: Foundational Aspects of SAT/SMT Solvers
Independence Results for the P vs. NP Question
Shai Ben David
University of Waterloo, Ontario, Canada
Foundations of Modern CDCL SAT Solver Implementation Niklas Een
University of California, Berkeley, USA
SMT Theory and DPLL(T) Albert Oliveras
Technical Univ. of Catalonia, Barcelona, Spain
Modern SMT Solver Implementation Leonardo DeMoura & Nikolaj BjornerMicrosoft Research, Redmond, USA
Approaches to Parallel SAT Solving Youssef Hamadi
Microsoft Research, Cambridge, UK
MaxSAT for Optimization Problems
Joao Marques-Silva
University College Dublin, Dublin, Ireland
Non-DPLL Approaches to Boolean SAT Solving Bart Selman & Carla Gomes
Cornell University, Ithaca, USA
SMT-LIB Initiative Cesare Tinelli
University of Iowa, Iowa City, USA
Complexity Theoretic Aspects of the Boolean SAT Problem Ryan Williams
IBM Almaden Research Center, San Jose, USA
Proof Complexity and Complexity of SAT Solvers
Sam Buss
University of California, San Diego, USA

Category 2: Description of SAT/SMT Solvers with tight focus on an application
Cryptography and SAT Solvers -- Why and How Mate Soos
Security Research Labs, Paris, France
Yices and Applications Bruno Dutertre
SRI International, Menlo Park, USA
CVC3 and Applications Clark Barrett
New York University, New York, USA
SAT4J: pseudo-boolean optimization & dependency management problems Daniel LeBerre
Université d'Artois, France
SAT-based Model-Checking Armin Biere
Johannes Kepler University, Linz, Austria
SAT solving in AI Henry Kautz
University of Rochester, Rochester, USA
Calculus of Data Structures for Verification and Synthesis
Viktor Kuncak & Ruzica Piskac
EPFL, Lausanne, Switzerland
Alloy/Kodkod and Applications Emina Torlak
LogicBlox, Atlanta, Georgia, USA
HAMPI: A Solver for String Theories Vijay Ganesh
MIT, Cambridge, USA
OpenSMT and Applications R. Bruttomesso & N. Sharygina
University of Lugano, Lugano, Switzerland
UCLID and Applications
Randy Bryant & Sanjit Seshia
CMU, Pittsburgh and UC, Berkeley, USA
MathSAT and Applications Alessandro Cimatti
Fondazione Bruno Kessler, Trento, Italy

Category 3: Description of tools using SAT/SMT Solvers
Sketching: Program Synthesis using SAT Solvers Armando Solar-Lezama
MIT, Cambridge, USA
BitBlaze & WebBlaze: Tools for computer security using SMT Solvers Dawn Song & Prateek Saxena
University of California, Berkeley, USA
SAGE: Automated Whitebox Fuzzing using SMT solvers
Patrice Godefroid & David Molnar
Microsoft Research, Redmond, USA
HAVOC: SMT solvers for precise and scalable reasoning of programs
Shuvendu Lahiri & Shaz Qadeer
Microsoft Research, Redmond, USA
Liquid Types: SMT Solver-based Types Ranjit Jhala
University of California, San Diego, USA
Scalable Testing/Reverse Engineering/Performance Profiling with Parallel and Selective Symbolic Execution
George Candea & Stefan Bucur
EPFL, Lausanne, Switzerland
Klee: An SMT Solver-based Dynamic Symbolic Testing Tool  Cristian Cadar
Imperial College London, London, UK
SAT-based Design Debugging
Sharad Malik
Princeton University, Princeton, USA
Harnessing SMT power using the verification engine Boogie
Rustan Leino
Microsoft Research, Redmond, USA
SMT Solver-based Compiler Optimization Verification
Sorin Lerner
University of California, San Diego, USA
CEGAR+SMT: Formal Verification of Control Logic in the Reveal System
Karem Sakallah
University of Michigan, Ann Arbor, USA
SAT Solvers for Formal Verification Ed Clarke
Carnegie Mellon University, Pittsburgh, USA
Symbolic Execution and Automated Exploit Generation David Brumley
Carnegie Mellon University, Pittsburgh, USA

The summer school is being held the week before the SAT conference 2011, which is slated to be held from June 19th to June 23rd, 2011 at Ann Arbor, Michigan, USA. The SMT Solver 2011 workshop (co-located with CAV 2011) will be held from July 14-15, 2011.

The main organizer of this summer school is Dr. Vijay Ganesh. Please direct all correspondences to him.