In the last few years there have been rapid developments in SMT solving for finite fields. These include new decision procedures, new implementations of SMT theory solvers, and new software verifiers that rely on SMT solving for finite fields. To support interoperability in this emerging ecosystem, we propose the SMT-LIB theory of finite field arithmetic (FFA). The theory defines a canonical representation of finite field elements as well as definitions of operations and predicates on finite field elements.
Modern SMT solvers, such as Z3, offer user-controllable strategies that allow solver users the ability to tailor solving strategies for their unique set of instances, thus dramatically enhancing the solver performance for their specific use cases. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address this problem of automated SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel heuristics allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across six important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42.7% more instances than the default strategy in Z3.
Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors? The main contribution of this work is the development of an efficient and user-friendly tool, , that solves a bunch of problems around model counting and sampling on the theory of bit-vectors, namely exact and approximate projected and non-projected model counting, along with the almost-uniform and uniform-like sampling. In the case of exact counting, projected counting, and uniform sampling, is the first tool to solve the problem—although all these problems have a lot of applications. Our tool converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. It keeps track of the variable mapping between the bitvector and CNF formula and passes that information to the CNF counter. We built our tool on top of SMT solver by integrating approximate model counter , exact model counter , almost-uniform sampler , and uniform-like sampler in it. Our experiments demonstrate significant performance improvements over existing methods.
The Alethe format has been adopted by several SMT solvers for explaining why a set of constraints is unsatisfiable. We describe how to interpret Alethe proof traces and generate corresponding proofs that are accepted by the Lambdapi proof checker, a foundational proof assistant based on dependent type theory and rewriting that is intended to serve as a pivot for exchanging proofs between interactive proof assistants. We give an overview of the encoding of SMT logic and of Alethe proof traces in Lambdapi and present results of the evaluation of the checker on benchmark examples.
The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with variousdecision procedures and extensions developed for it. However, recent works suggest that developing tailoredreasoning for some theories, such as sequences and strings, is more efficient than reasoning over them throughaxiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences asthey are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequencesand explore different ways to represent and reason over n-indexed sequences using existing theories, as well astailored calculi for the theory.
Zero-knowledge proof systems are becoming increasingly prevalent and being widely used to secure decentralized financial systems and protect the privacy of users. Given the sensitivity of these applications, zero-knowledge proof systems are a natural target for formal verification methods. We describe methods for checking one such proof system: Halo2. We use abstract interpretation and an SMT solver to check various properties of Halo2 circuits. Using abstract interpretation, we can detect unused gates, unconstrained cells, and unused columns. Using an SMT solver, we can detect under-constrained circuits (in the sense that for the same public input they have two efficiently computable satisfying assignments). This is the first work we are aware of that applies lightweight formal methods to PLONKish arithmetization and Halo2 circuits.
Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in automated reasoning to check the correctness of its internal systems and to provide assurances to customers. We are using SAT and SMT solvers more than one billion times a day, both for “real-time” queries in customer security (checking security policies and verifying network protections), and also for large queries involving code and hardware reasoning that are at the limits of what can be feasibly solved by current solvers. Supporting reasoning at this scale and volume requires careful examination of the problems to be solved and a clear focus on operations to ensure our analyses are consistently trustworthy and performant. I will describe some lessons learned and offer some directions for the community that should allow us to scale further, increase trust, and solve the next billion queries a day.
Dolmen provides tools to parse, type, and validate input files used in automated deduction, and in particular problems from the SMT-LIB . We present here an extension of Dolmen which makes it capable of verifying ground models for quantifier-free SMT-LIB problems. While most of the extension was a straightforward implementation of an evaluator for ground expressions, there were some challenges, related to corner cases of the semantics (division by zero, partial functions, ...), as well as order of evaluation of statements, most of which could be solved by improvements to the SMT-LIB standard for models.
This work attempts to choose quantifiers to instantiate based on a feedback from the SMT solver. This tackles the challenge that if a problem contains many quantifier expressions, it eventually gets flooded by too many generated ground terms. Therefore, we instantiate only some of the quantifiers but the question is, which are the useful ones? The SMT solver is modeled as a multi-armed bandit, where each quantifier is a lever producing a positive reward if an instantiation of the quantifier was useful. The issue is that we do not know whether an instantiation was useful or not until the given problem instance is actually proven (and then it’s too late). In this paper we explore several heuristics that attempt to assess the usefulness of quantifier instantiations.
Satisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security-critical applications. Therefore, being able to trust a solver’s results is crucial. One way to increase trust is to generate independently checkable proof certificates, which record the reasoning steps done by the solver. A key challenge with this approach is that it is difficult to efficiently and accurately produce proofs for reasoning steps involving term rewriting rules. Previous work showed how a domain-specific language, Rare , can be used to capture rewriting rules for the purposes of proof production. However, in that work, the Rare rules had to be trusted, as the correctness of the rules themselves was not checked by the proof checker. In this paper, we present I sa Rare , a tool that can automatically translate Rare rules into Isabelle/HOL lemmas. The soundness of the rules can then be verified by proving the lemmas. Because an incorrect rule can put the entire soundness of a proof system in jeopardy, our solution closes an important gap in the trustworthiness of SMT proof certificates. The same tool also provides a necessary component for enabling full proof reconstruction of SMT proof certificates in Isabelle/HOL. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT solver.
One of the few available complete methods for checking the satisfiability of sets of polynomial constraints over the reals is the cylindrical algebraic covering (CAlC) method. In this paper, we propose an extension for this method to exploit the strictness of input constraints for reducing the computational effort. We illustrate the concepts on a multidimensional example and provide experimental results to evaluate the usefulness of our proposed extension.
Let T be an SMT solver with no theory solvers except for Quantifier Instantiation. Given a set of first-order clauses S saturated by Resolution (with a valid literal selection function) we show that T is complete if its Trigger function is the same as the literal selection function. So if T halts with a ground model G, then G can be extended to a model in the theory of S. In addition for a suitable ordering, if all maximal literals are selected in each clause, then T will halt on G, so it is a decision procedure for the theory S. Also, for a suitable ordering, if all clauses are Horn, or all clauses are 2SAT, then T solves the theory S in polynomial time.
: Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. I will describe a series of works that develop a methodology for verifying distributed algorithms and systems using decidable logics, employing decomposition, abstraction, and user interaction. This methodology is implemented in an open-source tool, and has resulted in the first mechanized proofs of several important distributed protocols. I will also describe a novel approach to the problem of invariant inference based on a newly formalized duality between reachability and mathematical induction. The duality leads to a primal-dual search algorithm, and a prototype implementation already handles challenging examples that other state-of-the-art techniques cannot handle. I will briefly describe several other works, including a new optimization technique for deep learning computations that achieves significant speedups relative to existing deep learning frameworks.
The verification of deep neural networks is a recent algorithmic challenge that has attracted significant interest, resulting in a wide array of complete and incomplete solvers that draw on diverse techniques. As is typical in hard search problems, no single solver is expected to be the fastest on all inputs. While this insight has been leveraged to boost Boolean Satisfiability (SAT), for instance, by combining or tuning solvers, it is yet to lead to a leap in the neural network verification domain. Towards this goal, we present Goose , a meta-solver for deep neural network verification. Goose ’s architecture supports a wide variety of complete and incomplete solvers and leverages three key meta-solving techniques to improve efficiency: algorithm selection, probabilistic satisfiability inference, and time iterative deepening. Using Goose we observe an 47.3% improvement in PAR-2 score across over 800 benchmarks and 13 solvers from VNN-COMP ’21.
