ABSTRACT. CDSAT (Conflict-Driven Satisfiability) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length, which is an abstraction of the theory of arrays with length. The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved.

ABSTRACT. We present ongoing work on developing the user-propagator framework in SMT solving. We argue that the integration of user-propagators in SMT solving yields an efficient approach towards custom theory reasoning, without bringing fundamental changes in the underlining SMT architecture. We showcase our approach in the SMT solver Z3, provide practical evidence of our work, and also discuss potential venues for further improvements.

ABSTRACT. Constrained Horn Clauses (CHCs) are an intermediate program representation that can be generated by several verification tools, and that can be processed and solved by a number of Horn solvers. One of the main challenges when using CHCs in verification is the encoding of heap-allocated data-structures: such data-structures are today either represented explicitly using the theory of arrays, or transformed away with the help of invariants or refinement types, defeating the purpose of CHCs as a representation that is language-independent as well as agnostic of the algorithm implemented by the Horn solver. This paper presents an SMT-LIB theory of heaps tailored to CHCs, with the goal of enabling a standard interchange format for programs with heap data-structures. We introduce the syntax of the theory of heaps, define its semantics in terms of axioms and using a reduction to SMT-LIB arrays and data-types, provide an experimental evaluation and outline possible extensions and future work.

ABSTRACT. An interesting goal is for SMT solvers to produce independently checkable proofs. SMT languages already have expressive power that goes beyond first-order languages, and further extensions would give even more expressive power by allowing quantification over function types. Indeed, such extensions are considered in the current proposal for the new standard SMT3. Given the expressive power of SMT and its extensions, careful thought must be given to the intended semantics and an appropriate notion of proof. We propose higher-order set theory as an appropriate interpretation of SMT (and extensions) and obtain an adequate notion of SMT proofs via proof terms in higher-order set theory. To demonstrate the strength of this approach, we give a number of abstract examples that would be difficult to handle by other notions of proof. To demonstrate the practicality of the approach, we describe a family of integer difference logic examples. We give proof terms for each of these examples and check the correctness of the proofs using two proof checkers: the proof checker distributed with the Proofgold system and an alternative checker we have implemented that does not rely on access to the Proofgold block chain.

ABSTRACT. We present a simple resolution-based proof format targeted for SMT. The proof format uses a syntax similar to SMT-LIB terms. The resolution rule is its only proof rule with premises; all other rules are axioms proving tautological clauses. The format aims to be solver independent by only including a minimal complete set of axioms while still being able to express proofs succinctly. Most of its axioms are purely syntactic; only for arithmetic reasoning, some axioms with side conditions are used for succinct reasoning with linear (in)equalities. The format can be extended with solver-specific rules, which can then either be treated as trusted axioms, or, better, replaced by their low-level proof. The format has been implemented in the solver SMTInterpol and the solver produces proofs for all benchmarks it can solve in the combinations of the theories of equality, linear arithmetic, arrays and datatypes. There is also a stand-alone proof checker for this format.