SMT 2012: Papers with Abstracts

Papers
Practical Aspects of SAT Solving Armin Biere 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.
The Architecture of Inference from SMT to ETB Natarajan Shankar 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.
Program Verification as Satisfiability Modulo Theories Nikolaj Bjorner, Kenneth McMillan and Andrey Rybalchenko 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.
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers Sylvain Conchon, Guillaume Melquiond, Cody Roux and Mohamed Iguernelala 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.
Reasoning with Triggers Claire Dross, Sylvain Conchon, Johannes Kanig and Andrei Paskevich 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.
SMT-Based System Verification with DVF Amit Goel, Sava Krstic, Rebekah Leslie and Mark Tuttle 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.
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width Gergely Kovásznai, Andreas Fröhlich and Armin Biere 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.
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems Mohammad Abdul Aziz, Amr Wassal and Nevine Darwish 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.
Reachability Modulo Theory Library Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina 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.
SMT-LIB Sequences and Regular Expressions Nikolaj Bjorner, Vijay Ganesh, Raphaël Michel and Margus Veanes 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.
Exotic Semi-Ring Constraints Michael Codish, Yoav Fekete, Carsten Fuhs, Jürgen Giesl and Johannes Waldmann 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.
A Theory of Arrays with set and copy Operations Stephan Falke, Carsten Sinz and Florian Merz 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.
An SMT-based approach to automated configuration Raphaël Michel, Arnaud Hubaux, Vijay Ganesh and Patrick Heymans 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.
Anatomy of Alternating Quantifier Satisfiability (Work in progress) Anh-Dung Phan, Nikolaj Bjørner and David Monniaux 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.
The 2012 SMT Competition David Cok, Alberto Griggio, Roberto Bruttomesso and Morgan Deters 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.