ABSTRACT. Reasoning about complex SMT theories is still quite challenging, for instance bit-vectors, floating-point arithmetic, or strings. Approximations offer a means of mapping a complex theory into a simpler one, and attempting to reconstruct models or proofs in the original theory afterwards. UppSAT is an approximating abstract SMT-solver, based on the systematic approximation refinement framework. The framework can be instantiated using an approximation and a back-end SMT solver. Implemented in Scala, UppSAT is designed with easy and flexible specification of approximations in mind. We discuss the structure of approximations in UppSAT and the components needed for their specification. Because approximation components can be defined relatively independently, they can be flexibly combined to obtain many different flavours of approximation. In this extended abstract we discuss what kinds of approximations can be expressed in UppSAT, along with design choices that enable the modular mix-and-match specification of approximations. Finally, we also outline ideas for several new approximations and strategies which we are currently working on (with first results expected to be available at the workshop).

ABSTRACT. Alt-Ergo is an SMT solver jointly developed by Université Paris-Sud and the OCamlPro company. The first version was released in 2006. Since then, its architecture has been continuously adapted for proving formulas generated by software development frameworks. As type systems with polymorphism arise naturally is such platforms, the design of Alt-Ergo has been guided (and constrained) by a native -- and non SMT-LIB compliant -- input language for a polymorphic first-order logic.

In this paper, we present the last version of Alt-Ergo, its architecture and main features. The main recent work is a support for a conservative polymorphic extension of the SMT-LIB 2 standard. We measure Alt-Ergo’s performances with this new frontend on a set of benchmarks coming from the deductive program verification systems Frama-C, SPARK 2014, Why3 and Atelier-B, as well as from the SMT-LIB benchmarks library.

ABSTRACT. In our previous papers, we investigated several aspects of applying Optimization Modulo Theories (OMT) solvers to Wireless Sensor Networks (WSNs). None of the solvers we used in our experiments scaled enough for WSNs of common size in practice. This is particularly true when investigating additional dependability and security constraints on WSNs of high density. In this paper, we propose an idea of speeding up the OMT solving process by taking into consideration some resources in the systems and by applying regression analysis on those resource values. For instance, in WSNs, the electrical charge in the batteries of sensor nodes can be considered to be a resource that is being consumed as approaching the maximal lifetime of the network. Another example is the knapsack problem where the remaining capacity of the knapsack can be used as such a resource. We show how to integrate this idea in search algorithms in the OMT framework and introduce a new OMT solver called Puli. We present experiments with Puli on WSN and knapsack benchmarks, which show remarkable improvements in the number of solved instances as well as computation time compared to existing solvers. Furthermore, we show that further significant improvement can be realized on so-called monotonous problems, such as WSN optimization, for which Puli can generate more precise assertions. We present Puli as a work-in-progress prototype that we are planning to upgrade to an official release soon, which we want to make publicly available.

ABSTRACT. Ethereum smart contracts are programs that run inside a public distributed database called a blockchain. These smart contracts are used to handle tokens of value, can be accessed and analyzed by everyone and are immutable once deployed. Those characteristics make it imperative that smart contracts are bug-free at deployment time, hence the need to verify them formally. In this paper we describe our current efforts in building an SMT-based formal verification module within the compiler of Solidity, a popular language for writing smart contracts. The tool is seamlessly integrated into the compiler, where during compilation, the user is automatically warned of and given counterexamples for potential arithmetic overflow/underflow, unreachable code, trivial conditions, and assertion fails. We present how the component currently translates a subset of Solidity into SMT statements using different theories, and discuss future challenges such as multi-transaction and state invariants.

ABSTRACT. The logic of Constrained Horn Clauses (CHC) provides an effective logical characterization of many problems in (software) verification. For example, CHC naturally capture inductive invariant discovery for sequential programs, compositional verification of concurrent and distributed systems, and verification of program equivalence. CHC is used as an intermediate representation by several state-of-the-art program analysis tools, including SeaHorn and JayHorn.

Existing CHC solvers, such as Spacer and Eldarica, are limited to discovering quantifier free solutions. This severely limits their applicability in software verification where memory is modelled by arrays and quantifiers are necessary to express program properties. In this work, we extend the IC3 framework (used by Spacer CHC solver) to discover quantified solutions to CHC. Our work addresses two major challenges: (a) finding a sufficient set of instantiations that guarantees progress, and (b) finding and generalizing quantified candidate solutions. We have implemented our algorithm in Z3 and describe experiments with it in the context of software verification of C programs.

ABSTRACT. In this paper, we explore a development paradigm where rewrite rules are suggested to the SMT solver developer using syntax-guided enumeration. We capitalize on the recent advances in enumerative syntax-guided synthesis (SyGuS) techniques for efficiently enumerating terms in a grammar of interest, and novel sampling techniques for testing equivalence between terms. We present our preliminary experience with this feature in the SMT solver CVC4, showing its impact on its rewriting capabilities using several internal metrics, and its subsequent impact on solving bit-vector and string constraints in applications.

ABSTRACT. Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT (HOSMT) is still little explored. In this preliminary report we discuss how to extend SMT solvers to natively support higher-order reasoning without compromising their performances on FO problems. We present a pragmatic extension to the cvc4 solver in which we generalize existing data structures and algorithms to HOSMT, thus leveraging the extensive research and implementation efforts dedicated to efficient FO solving. Our evaluation shows that the initial implementation does not add significant overhead to FO problems and its performance is on par with the encoding-based approach for HOSMT. We also discuss an alternative extension being implemented in veriT, in which new data structures and algorithms are being developed from scratch to best support HOSMT, thus avoiding the inherent difficulties of generalizing in a graceful way existing infrastructure not indented to higher-order reasoning.

ABSTRACT. MCSAT is an approach to SMT-solving that uses assignments of values to first-order variables in order to try and build a model of the input formula. When different theories are combined, as formalized in the CDSAT system, equalities between variables and terms play an important role, each theory module being required to understand equalities and which values are equal to which. This paper broaches the topic of how to reason about equalities in a centralized way, so that the theory reasoners can avoid replicating equality reasoning steps, and even benefit from a centralized implementation of equivalence classes of terms, which is based on a equality graph (Egraph). This paper sketches the design of a prototype based on this architecture.

ABSTRACT. We propose an automated theorem prover that combines an SMT solver with tableau calculus and rewriting. Tableau inference rules are used to unfold propositional content into clauses while atomic formulas are handled using satisfiability decision procedures as in traditional SMT solvers. To deal with quantified first order formulas, we use metavariables and perform rigid unification modulo equalities and rewriting, for which we introduce an algorithm based on superposition, but where all clauses contain a single atomic formula. Rewriting is introduced along the lines of deduction modulo theory, where axioms are turned into rewrite rules over both terms and propositions. Finally, we assess our approach over a benchmark of problems in the set theory of the B method.

ABSTRACT. Many areas of automated reasoning are goal-oriented i.e the aim is to prove a goal from a set of axioms. Some methods, including the method of saturation-based reasoning explored in this paper, do not rely on having an explicit goal but can employ specific heuristics if one is present. SMT-LIB problems do not record a specific goal, meaning that we cannot straightforwardly employ goal-oriented proof search heuristics. In this work we examine methods for identifying the potential goal in an SMT-LIB problem and evaluate (using the Vampire theorem prover) whether this can help theorem provers based saturation-based proof search.