SMT 2012: Papers with AbstractsPapers 

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 tacticsbased interactive theorem provers. Prior work has mostly focused on finegrained modular inference. However, with the availability of a diverse range of highquality 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 coarsegrained 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, SMTLIB, and a growing set of benchmarks sharing this common format. SMTLIB captures very well an interface that is suitable for many tasks that reduce to solving firstorder formulas modulo theories. Here we propose to extend these benefits into the domain of symbolic software model checking. We make a case that SMTLIB 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 frontends, from developing algorithms for solving constraints over recursive predicates.  Abstract. The treatment of the axiomatic theory of floatingpoint 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 AltErgo SMT solver.  Abstract. SMT solvers can decide the satisfiability of ground formulas modulo a combination of builtin theories. Adding a builtin 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 firstorder 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 firstorder 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 builtin operations are consistent with SMTLIB, as are the multisorted firstorder logical formulas that may occur in DVF programs as pre and postconditions, 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 assumeguarantee scheme supports a thin layer of interactive proving.  Abstract. Bitprecise reasoning is important for many practical applications of Satisfiability Modulo Theories (SMT). In recent years efficient approaches for solving fixedsize bitvector formulas have been developed. From the theoretical point of view, only few results on the complexity of fixedsize bitvector logics have been published. In this paper we show that some of these results only hold if unary encoding on the bitwidth of bitvectors is used. We then consider fixedsize bitvector logics with binary encoded bitwidth and establish new complexity results. Our proofs show that binary encoding adds more expressiveness to bitvector logics, e.g. it makes fixedsize bitvector logic even without uninterpreted functions nor quantication NExpTimecomplete. 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 infinitestate systems plays a central role in many verification tasks. In the last decade, SMTSolvers 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 SMTLIB format. This paper is a first proposal for a new SMTbased verification language that is suitable for defining transition systems and safety properties.  Abstract. Strings are ubiquitous in software. Tools for specification, verification and testcase 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 SMTLIBization 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 semiring 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 bitblasting 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 bitblasting, improving on previous proposals to apply binary bitblasting. Moreover, our results indicate that, for our benchmarks, unary bitblasting 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 userspecified 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 SMTsolvers 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 SMTTEST 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 unsatcoregeneration track and encouraged the demonstration of proofgeneration solvers. The series of competitions is expected to be continued at SAT 2013. 

