SMT 2010
Quick Links
Background
Programme
Proceedings
Committees
Student Travel Awards
Sponsors
CAV 2010
SAT 2010
The
Ross Fountain
Edinburgh
Previous Editions
SMT 2009
SMT 2008
SMT 2007
PDPAR 2006
PDPAR 2005
PDPAR 2004
PDPAR 2003
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 first-order formulas modulo background
theories, known as the Satisfiability Modulo Theories (SMT) problem, has
proved to be an enabling technology for verification, test-vector generation,
compiler optimization, scheduling, and other areas.
The success of SMT techniques depends on the development of both
domain-specific decision procedures for each concrete theory
(e.g., linear arithmetic, the theory of arrays, or the theory of
bit-vectors) and combination methods that allow one to obtain more versatile
SMT tools. These two ingredients together make SMT techniques well-suited
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
09:00-10:00
(SAT SMT Tutorial)
09:00-10:00
I N V I T E D T A L K
Silvio Ghilardi
, U Milano
SMT model checking for
array-based systems
B R E A K
10:30-11:30
I N V I T E D T A L K
Nikolai Tillmann
, Microsoft
SMT-Solvers In (Tracing) Just-in-Time Compilers
10:30-11:00
M. Ganai, F. Ivancic
Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC
11:00-11:30
E. Abraham, U. Loup, F. Corzilius, T. Sturm.
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra
11:30-12:00
Frederic Besson
On using an inexact floating-point LP solver for deciding linear
arithmetic in a SMT solver
11:30-12:00
B. Paleo, S. Merz, P. Fontaine
Exploring and Exploiting Algebraic and Graphical Properties of Resolution
12:00-12:30
M. Bankovic and F. Maric
Alldifferent Constraint Solver in SMT
12:00-12:30
P. Rümmer and T. Wahl
An SMT-LIB Theory of Binary Floating-Point Arithmetic
L U N C H B R E A K
14:00-14:20
Joint Session with SAT
(SAT paper)
14:00-14:30
D. Jovanovic and C. Barrett.
Sharing is Caring
14:20-14:50
J. Christ, J. Hoenicke
Instantiation-Based Interpolation for Quantified Formulae
14:30-15:00
L. Cordeiro, B Fischer
Bounded Model Checking of Multi-threaded Software using SMT
solvers
B R E A K
15:30-16:00
C. Barrett, A. Stump, C. Tinelli
The SMT-LIB Standard – Version 2.0
15:30-16:00
A. Griggio
A Practical Approach to SMT(LA(Z))
16:00-17:00
Business meeting
16:00-16:30
A. Reynolds, L. Hadarean, C. Tinelli, Y. Ge, A. Stump, C. Barrett
Comparing Proof Systems for Linear Real Arithmetic with LFSC
16:30-17: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.
The selection between FMSD and JSAT will be based on the scope of the paper prior
to the reviewing process.
Programme Committee
Clark Barrett
, New York University
Armin Biere
, Johannes Kepler University Linz
Nikolaj Bjørner
, Microsoft Research
Alessandro Cimatti
, ITC-IRST, Trento
Leonardo de Moura
, Microsoft Research
Bruno Dutertre
, SRI International
Aarti Gupta
, NEC (co-chair)
Himanshu Jain
, Synopsys
Daniel Kroening
, Oxford University (co-chair)
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.
US