[go: up one dir, main page]

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 de­ci­sion 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 auto­mated 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 en­cour­aged. 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 work­shop.

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:00Business 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, de­pen­ding on the paper's subject:

The selection between FMSD and JSAT will be based on the scope of the paper prior to the reviewing process.

Programme Committee

Student Travel Awards

To be announced.

Sponsors

To be announced.