WORKSHOP: SAT/SMT Solvers

Boolean SAT/SMT 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, computer security, AI and biology. Given the rather dramatic explosion in the usage scenarios of SAT/SMT solvers, there is great demand for newer kinds of features and higher levels of performance required of these solvers. This session will highlight recent developments around SMT, MAX-SAT, and parallel SAT engines.

Speaker Details

I am managing the Foundations of Software Engineering group at Microsoft Research in Redmond. Our projects span logics for authentication, model programs, dynamic symbolic execution, model-based software design, and symbolic solvers. My current main work is around the state-of-the-art Satisfiability Modulo Theories solver Z3, jointly with Leonardo de Moura. In a previous life I also shipped distributed file system replication and remote compression products. I received my Ph.D. from Stanford University in 1998.

Joao Marques-Silva is Stokes Professor of Computer Science and Informatics at University College Dublin (UCD), Ireland. Before moving to UCD, he held appointments at the University of Southampton, UK, and at the Technical University of Lisbon, Portugal. Joao Marques-Silva holds a PhD degree in Electrical Engineering and Computer Science from the University of Michigan, Ann Arbor, in 1995, and the Habiliation degree in Computer Science from the Technical University of Lisbon, Portugal, in 2004. His research interests include algorithms for constraint solving and optimization, and applications in formal methods, artificial intelligence, and bioinformatics. He received the 2009 CAV award for fundamental contributions to the development of high-performance Boolean satisfiability solvers.

Youssef Hamadi leads the Constraint Reasoning Group in Microsoft Research Cambridge. He is also the founder and co-director of the Microsoft-CNRS chair Optimisation for Sustainable Development, at École Polytechnique. His current research considers the design of complex systems based on multiple formalisms feed by different information channels which plan ahead and perform smart decisions. This work is set at the intersection of Optimization and Artificial Intelligence. Currently, his focus is on Autonomous Search, Parallel Search, and Propositional Satisfiability, with applications to software-verification, Automated Planning and business intelligence.

Date:
Speakers:
Nikolaj Bjorner, Joao Marques-Silva, and Youssef Hamadi
Affiliation:
Microsoft Research, UCD, MSRC