SMT 2012:Papers with Abstracts

Papers
Abstract. SAT solving techniques are used in many automated reasoning engines. This talk gives an overview on recent developments in practical aspects of SAT solver development. Beside improvements of the basic conflict driven clause learning (CDCL) algorithm, we also discuss improving and integrating advanced preprocessing techniques as inprocessing during search. The talk concludes with a brief overview on current trends in parallelizing SAT.
Abstract. Modularity plays a central role in logical reasoning. We want to be
able to reuse proofs, proof patterns, theories, and specialized
reasoning procedures. Architectures that support modularity have been
developed at all levels of inference: SAT solvers, theory solvers,
combination solvers and rewriters, SMT solvers, simplifiers, rewriters,
and tactics-based interactive theorem provers. Prior work has mostly
focused on fine-grained modular inference. However, with the
availability of a diverse range of high-quality inference tools, it has
become important to systematically integrate these big components into
robust toolchains. At SRI, we have been developing a framework called
the Evidential Tool Bus (ETB) as a distributed platform for the
coarse-grained integration of inference components into flexible,
scriptable workflows. The talk describes the architecture of ETB along
with some motivating applications.
Abstract. A key driver of SMT over the past decade has been an interchange format, SMT-LIB,
and a growing set of benchmarks sharing this common format.
SMT-LIB captures very well an interface that is suitable
for many tasks that reduce to solving first-order formulas modulo theories.
Here we propose to extend these benefits into the domain of symbolic
software model checking. We make a case that SMT-LIB can
be used, and to a limited extent adapted, for exchanging symbolic
software model checking benchmarks. We believe this layer facilitates
dividing innovations in modeling, developing program logics and front-ends,
from developing algorithms for solving constraints over recursive predicates.
Abstract. The treatment of the axiomatic theory of floating-point numbers is
out of reach of current SMT solvers, especially when it comes to
automatic reasoning on approximation errors. In this paper, we
describe a dedicated procedure for such a theory, which provides an
interface akin to the instantiation mechanism of an SMT solver.
This procedure is based on the approach of the Gappa tool: it
performs saturation of consequences of the axioms, in order to
refine bounds on expressions. In addition to the original approach,
bounds are further refined by a constraint solver for linear
arithmetic. Combined with the natural support for equalities
provided by SMT solvers, our approach improves the treatment of
goals coming from deductive verification of numeric programs. We
have implemented it in the Alt-Ergo SMT solver.
Abstract. SMT solvers can decide the satisfiability of ground formulas modulo a combination of
built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures.
In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate using the theory of arrays, how such proofs can be achieved in our formalism.
Abstract. We introduce the <i>Deductive Verificaton Framework</i> (DVF), a language and a tool for verifying properties of transition systems. The language is procedural and the system transitions are a selected subset of procedures. The type system and built-in operations are consistent with SMT-LIB, as are the multisorted first-order logical formulas that may occur in DVF programs as pre- and post-conditions, assumptions, assertions, and goals. A template mechanism allows parametric specification of complex types within the confines of this logic. Verification conditions are generated from specified goals and passed to SMT engine(s). A general assume-guarantee scheme supports a thin layer of interactive proving.
Abstract. Bit-precise reasoning is important for many practical applications of
Satisfiability Modulo Theories (SMT). In recent years efficient approaches
for solving fixed-size bit-vector formulas have been developed. From
the theoretical point of view, only few results on the complexity of
fixed-size bit-vector logics have been published. In this paper we show
that some of these results only hold if unary encoding on the bit-width of
bit-vectors is used. We then consider fixed-size bit-vector logics with
binary encoded bit-width and establish new complexity results. Our proofs
show that binary encoding adds more expressiveness to bit-vector logics,
e.g. it makes fixed-size bit-vector logic even without uninterpreted
functions nor quantication NExpTime-complete. We also show that under
certain restrictions the increase of complexity when using binary encoding
can be avoided.
Abstract. In this paper we present an approach for measuring the hardness of SMT problems.
We present the required features, the statistical hardness model used and the machine
learning technique which we used. We apply our method to estimate the hardness of
problems in Quantier Free Bit Vector (QFBV) theory and we used four of the contesting
solvers in SMT2011 to demonstrate our technique. We have qualitatively expanded some
propositional SAT features existing in the literature to directly work on general SMT
problem instances without preprocessing. The results show that our work is a promising
proof of concept.
Abstract. Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.
Abstract. Strings are ubiquitous in software. Tools for specification,
verification and test-case generation of software rely in various degrees on
representing and reasoning about strings. Reasoning about strings is
particularly important in several security critical applications, such as
web sanitizers. Besides a basic representation of strings, applications
also use string recognizers and transducers.
This paper presents a proposal for an SMT-LIBization of strings and regular
expressions. It introduces a theory of sequences, generalizing strings,
and builds a theory of regular experssions on top of sequences.
The logic QF_BVRE is designed to capture a common substrate among
existing tools for string constraint solving.
Abstract. Exotic semi-ring constraints arise in a variety of applications and
in particular in the context of automated termination analysis.

We propose two techniques to solve such constraints: (a) to model
them using Boolean functions and integer linear arithmetic and solve
them using an SMT solver (QF_LIA, in certain cases also QF_IDL);
and (b) to seek finite domain solutions by applying unary bit-blasting
and solve them using a SAT solver.

In this note, we show the structure of such systems of constraints,
and report on the performance of SMT solvers and SAT encodings when
solving them. In particular, we observe that good results are
obtained by unary bit-blasting, improving on previous proposals to
apply binary bit-blasting. Moreover, our results indicate that, for
our benchmarks, unary bit-blasting leads to better results than the
ones directly obtained by an SMT solver.
Abstract. The theory of arrays is widely used in order to model main memory in program analysis, software verification, bounded model checking, symbolic execution, etc. Nonetheless, the basic theory as introduced by McCarthy is not expressive enough for important practical cases since it only supports array updates at single locations. In programs, the memory is often modified using functions such as memset or memcpy/memmove, which modify a user-specified range of locations whose size might not be known statically. In this paper we present an extension of the theory of arrays with set and copy operations which make it possible to reason about such functions. We also discuss further applications of the theory.
Abstract. We present a novel use of SMT solvers: configuration problems. Configuration problems are everywhere and particularly in product lines, where different yet similar products can be built from a common set of assets, which are then chosen, specialized and combined to form a product. Designing a product line boils down to enumerate the different parts of the products and the rules for combining them. These rules are often expressed as constraints. Various categories of constraint solvers exist, but SMT-solvers appear to be a solution of choice for configuration problem. In this paper, we present the configuration problem, we briefly introduce how we represent this type of problem and we map this representation to the input language of an STP solver able to support the various types of constraints found in configuration problems.
Abstract. We report on work in progress to generalize an algorithm recently introduced in [10] for checking
satisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures:
a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminating
or partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmetic
formulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report on
experiments on different variants of the auxiliary procedures. So far, there is an edge to applying
SMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantified
variables per round is almost as good. Both approaches offer drastic improvements to applying
default quantifier elimination.
Abstract. The 2012 SMT Competition was held in conjunction with the SMT workshop at IJCAR 2012. Eleven solvers participated, showing improvements over 2011 in some but not all divisions. The competition featured a new unsat-core-generation track and encouraged the demonstration of proof-generation solvers. The series of competitions is expected to be continued at SAT 2013.