SMT 2010
8th International Workshop on Satisfiability Modulo Theories
Affiliated with CAV 2010 and SAT 2010
July 14–15, 2010
Edinburgh
Background
Determining the satisfiability of firstorder formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, testvector generation, compiler optimization, scheduling, and other areas.
The success of SMT techniques depends on the development of both domainspecific decision procedures for each concrete theory (e.g., linear arithmetic, the theory of arrays, or the theory of bitvectors) and combination methods that allow one to obtain more versatile SMT tools. These two ingredients together make SMT techniques wellsuited for use in larger automated reasoning and formal verification efforts.
Aims and Scope
The aim of this workshop is to bring together researchers working on SMT and users of SMT techniques. Relevant topics include but are not limited to:
 New decision procedures and new theories of interest
 Combinations of decision procedures
 Novel implementation techniques
 Benchmarks and evaluation methodologies
 Applications and case studies
 Theoretical results
Papers on pragmatical aspects of implementing and using SMT tools are especially encouraged. Furthermore, we are especially encouraging submissions on the use of SMT in systems verification, and there will be a special issue of FMSD dedicated specifically to the papers on this topic. The chairs will be happy to clarify whether a particular topic is suitable for the workshop.
Programme
July 14th  July 15th  

(SAT SMT Tutorial) 
I N V I T E D T A L K Silvio Ghilardi, U Milano SMT model checking for arraybased systems 

B R E A K  
I N V I T E D T A L K Nikolai Tillmann, Microsoft SMTSolvers In (Tracing) JustinTime Compilers  10:3011:00 
M. Ganai, F. Ivancic Efficient Decision Procedure for Nonlinear Arithmetic Constraints using CORDIC 

11:0011:30 
E. Abraham, U. Loup, F. Corzilius, T. Sturm. A Lazy SMTSolver for a NonLinear Subset of Real Algebra 

11:3012:00 
Frederic Besson On using an inexact floatingpoint LP solver for deciding linear arithmetic in a SMT solver  11:3012:00 
B. Paleo, S. Merz, P. Fontaine Exploring and Exploiting Algebraic and Graphical Properties of Resolution 

12:0012:30 
M. Bankovic and F. Maric Alldifferent Constraint Solver in SMT  12:0012:30 
P. Rümmer and T. Wahl An SMTLIB Theory of Binary FloatingPoint Arithmetic 

L U N C H B R E A K  
14:0014:20 
Joint Session with SAT
(SAT paper)  14:0014:30 
D. Jovanovic and C. Barrett. Sharing is Caring 

14:2014:50 
J. Christ, J. Hoenicke InstantiationBased Interpolation for Quantified Formulae  14:3015:00 
L. Cordeiro, B Fischer Bounded Model Checking of Multithreaded Software using SMT solvers 

B R E A K  
15:3016:00 
C. Barrett, A. Stump, C. Tinelli The SMTLIB Standard – Version 2.0  15:3016:00 
A. Griggio A Practical Approach to SMT(LA(Z)) 

16:0017:00  Business meeting  16:0016:30 
A. Reynolds, L. Hadarean, C. Tinelli, Y. Ge, A. Stump, C. Barrett Comparing Proof Systems for Linear Real Arithmetic with LFSC 

16:3017:00  A report on the SMT Competition 
Proceedings
Only informal proceedings will be distributed at the workshop. Papers presented at SMT 2010 will be considered for one of two special issues of the following journals, depending on the paper's subject:
 There will be a special issue of FMSD for those papers addressing applications of SMT in systems verification.
 There will be a special issue of JSAT for the algorithmic/theory papers.
Programme Committee
 Clark Barrett, New York University
 Armin Biere, Johannes Kepler University Linz
 Nikolaj Bjørner, Microsoft Research
 Alessandro Cimatti, ITCIRST, Trento
 Leonardo de Moura, Microsoft Research
 Bruno Dutertre, SRI International
 Aarti Gupta, NEC (cochair)
 Himanshu Jain, Synopsys
 Daniel Kroening, Oxford University (cochair)
 Sava Krstic, Intel Corporation
 David Monniaux, Verimag
 Philipp Rümmer, Oxford University
 Roberto Sebastiani, Universita di Trento
 Cesare Tinelli, University of Iowa
Student Travel Awards
To be announced.
Sponsors
To be announced.