NEW: Student travel grants available.
Click here for more information.
Abstract
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,
synthesis, test generation, compiler optimization, scheduling, and
other areas. The success of SMT techniques depends on the development
of both domain-specific decision procedures for each background 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, usually leveraging Boolean satisfiability (SAT)
solvers. These ingredients together make SMT techniques well-suited
for use in larger automated reasoning and verification efforts.
The aim of the SMT 2011 workshop is to bring together researchers
working on SMT and users of SMT solvers. Topics of interest include
but not limited to new theories, decision procedures, novel
implementation techniques, applications, and evaluation techniques.
Aims and Scope
The aim of the SMT 2011 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 pragmatic aspects of implementing and using SMT tools are
especially encouraged.
Important Dates
- Submission deadline: April 15, 2011
- Notification of acceptance/rejection: May 20, 2011
- Final version due: June 10, 2011
- Workshop: July 14-15, 2011