[an error occurred while processing this directive] Introduction [an error occurred while processing this directive]
Home - Intro - Login - Public results - Specs - Thanks - SMT-LIB - SMT-COMP

Introduction

Decision procedures. Decision procedures for satisfiability modulo theories (SMT) are of continuing interest for many verification applications. SMT solvers are typically used for verification as backends: a verification problem or subproblem is translated into an SMT formula and submitted to the SMT solver. The solver then attempts to report satisfiability or unsatisfiability of the formula. The advantage SMT solvers are usually considered to have over pure SAT solvers, which are also often used as verification backends (e.g., for bounded model checking), is the higher level of abstraction at which they can operate. By implementing theories like arithmetic, arrays, and uninterpreted functions directly, SMT solvers have the promise to provide higher performance than SAT solvers working on encodings of such structures to the bit level.

Standard formats. The additional promise of SMT over pure SAT is balanced by additional challenges. Since SMT deals with first-order (most commonly quantifier-free) formulas instead of purely propositional ones, creation and widespread adoption of a common input language is more difficult than for SAT. It is furthermore more important, since the more expressive setting of SMT potentially allows more room for variation in the exact details of the logic (e.g., sorted or unsorted, total or partial functions, etc.). Hence, translations between input formats of different tools are more complex, and in some cases it may even not be clear what such a translation should be. This makes the issue of input format critical. For combination with other tools like skeptical proof assistants (requiring a proof of every theorem validated by an external tool), common output formats for objects like proofs and models are also necessary for the adoption of SMT.

Competition. The Satisfiability Modulo Theories Competition (SMT-COMP) arose from the SMT-LIB (``Satisfiability Modulo Theories Library'') initiative to spur adoption of the common, community-designed SMT-LIB formats, and to spark further advances in SMT, especially for verification. Competitions in other automated reasoning fields, such as CASC and the SAT competition, have helped inspire continuing improvements in tools from year to year. The first SMT-COMP was held in 2005 as a satellite event of the 17th International Conference on Computer-Aided Verification (CAV). The experience with SMT-COMP 2005 confirmed the community's expectations that a public competition would indeed motivate implementors of SMT solvers to adopt the common SMT-LIB input format. The second SMT-COMP, held as a satellite event of CAV 2006, provided further evidence that such a competition can stimulate improvement in solver implementations: solvers entered in SMT-COMP 2006 were significantly improved over the winning implementations of SMT-COMP 2005.

SMT-Exec. The Satisfiability Modulo Theories Execution Service (SMT-Exec) is a solver execution service provided by the SMT-LIB initiative for the benefit of the SMT community. Using the computational hardware from SMT-COMP’07 and a similar interface, SMT-Exec permits members of the SMT community:

Experiments and uploaded solvers may be kept private to a user account, or “published” to the website so that they may be viewed and used by all SMT community members.

[an error occurred while processing this directive]
Home - Intro - Login - Public results - Specs - Thanks - SMT-LIB - SMT-COMP

Last modified: Tue 09 Feb 2016 16:01 CST
Valid XHTML 1.0 Valid CSS!