ABSTRACT. Separation logic (SL) has gained widespread popularity as a formal foundation of tools that analyze and verify heap-manipulating programs. Its great asset lies in its assertion language, which can succinctly express how data structures are laid out in memory, and its discipline of local reasoning, which mimics human intuition about how to prove heap programs correct. This talk discusses approaches to automated reasoning in separation logics using SMT solvers. I will present fragments of SL that admit reductions to decidable first-order theories. I will also discuss incomplete approaches based on combinations of SL-style proof-theoretic reasoning and SMT techniques for some nonstandard models of SL. These techniques have been implemented in the deductive program verifier GRASShopper.

ABSTRACT. Formal methods applications often rely on SMT solvers to automatically discharge proof obligations. SMT solvers handle quantified formulas using incomplete heuristic techniques like E-matching, and often resort to model-based quantifier instantiation (MBQI) when these techniques fail. This paper revisits enumerative instantiation, a technique that considers instantiations based on exhaustive enumeration of ground terms. Although simple, we argue that enumerative instantiation can supplement other instantiation techniques and be a viable alternative to MBQI for valid proof obligations. We first present a stronger Herbrand Theorem, better suited as a basis for the instantiation loop used in SMT solvers; it furthermore requires considering less instances than classical Herbrand instantiation. Based on this result, we present different strategies for combining enumerative instantiation with other instantiation techniques in an effective way. The experimental evaluation shows that the implementation of these new techniques in the SMT solver cvc4 leads to significant improvements in several benchmark libraries, including many stemming from verification efforts.

ABSTRACT. An effective approach to handling the theory of floating- point is to reduce it to the theory of bit-vectors. Implementing the re- quired encodings is complex, error prone and require a deep understand- ing of floating-point hardware. This paper presents SymFPU, a library of encodings that can be included in solvers. It also includes a verification argument for its correctness, and experimental results showing that its use in CVC4 out-performs all previous tools. As well as a significantly improved performance and correctness, it is hoped this will give a simple route to add support for the theory of floating-point.

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. 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. 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.