More Like this

1. Scalable Bit-Blasting with Abstractions

   https://doi.org/10.1007/978-3-031-65627-9_9  

   Niemetz, Aina; Preiner, Mathias; Zohar, Yoni (January 2024, Springer Nature Switzerland)

   Gurfinkel, Arie; Ganesh, Vijay (Ed.)

   Abstract The dominant state-of-the-art approach for solving bit-vector formulas in Satisfiability Modulo Theories (SMT) is bit-blasting, an eager reduction to propositional logic. Bit-blasting is surprisingly efficient in practice but does not generally scale well with increasing bit-widths, especially when bit-vector arithmetic is present. In this paper, we present a novel CEGAR-style abstraction-refinement procedure for the theory of fixed-size bit-vectors that significantly improves the scalability of bit-blasting. We provide lemma schemes for various arithmetic bit-vector operators and an abduction-based framework for synthesizing refinement lemmas. We extended the state-of-the-art SMT solver Bitwuzla with our abstraction-refinement approach and show that it significantly improves solver performance on a variety of benchmark sets, including industrial benchmarks that arise from smart contract verification. 

   more » « less
2. Interpolation and Model Checking for Nonlinear Arithmetic

   Jovanović, Dejan; Dutertre, Bruno (July 2021, Computer Aided Verification 33rd International Conference, CAV 2021)

   Silva, Alexandra; Leino, Rustan (Ed.)

   We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic. 

   more » « less
3. Lean-SMT: An SMT Tactic for Discharging Proof Goals in Lean

   https://doi.org/10.1007/978-3-031-98682-6_11  

   Mohamed, Abdalrhman; Mascarenhas, Tomaz; Khan, Harun; Barbosa, Haniel; Reynolds, Andrew; Qian, Yicheng; Tinelli, Cesare; Barrett, Clark (July 2025, Springer Nature Switzerland)

   Piskac, Ruzica; Rakamarić, Zvonimir (Ed.)

   Abstract Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to prove a translated proof goal and the reconstruction of the resulting proof into valid justifications for the original goal. We presentlean-smt, a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer’s SMT integration, with promising results. We also evaluatelean-smtas a standalone proof checker for proofs of SMT-LIB problems. We show thatlean-smtoffers a smaller trusted core without sacrificing too much performance. 

   more » « less
4. A Decidable Logic for Tree Data-Structures with Measurements

   https://doi.org/10.1007/978-3-030-11245-5_15  

   Qiu, Xiaokang; Wang, Yanjun (January 2019, 20th International Conference on Verification, Model Checking, and Abstract Interpretation)

   We present DRYADdec, a decidable logic that allows reasoning about tree data-structures with measurements. This logic supports user-defined recursive measure functions based on Max or Sum, and recursive predicates based on these measure functions, such as AVL trees or red-black trees. We prove that the logic’s satisfiability is decidable. The crux of the decidability proof is a small model property which allows us to reduce the satisfiability of DRYADdec to quantifier-free linear arithmetic theory which can be solved efficiently using SMT solvers. We also show that DRYADdec can encode a variety of verification and synthesis problems, including natural proof verification conditions for functional correctness of recursive tree-manipulating programs, legality conditions for fusing tree traversals, synthesis conditions for conditional linear-integer arithmetic functions. We developed the decision procedure and successfully solved 220+ DRYADdec formulae raised from these application scenarios, including verifying functional correctness of programs manipulating AVL trees, red-black trees and treaps, checking the fusibility of height-based mutually recursive tree traversals, and counterexample-guided synthesis from linear integer arithmetic specifications. To our knowledge, DRYADdec is the first decidable logic that can solve such a wide variety of problems requiring flexible combination of measure-related, data-related and shape-related properties for trees. 

   more » « less
5. Satisfiability Modulo Theories: A Beginner’s Tutorial

   https://doi.org/10.1007/978-3-031-71177-0_31  

   Barrett, Clark; Tinelli, Cesare; Barbosa, Haniel; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni (September 2024, Springer Nature Switzerland)

   Platzer, Andre; Rozier, Kristin Yvonne; Pradella, Matteo; Rossi, Matteo (Ed.)

   Abstract Great minds have long dreamed of creating machines that can function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power and automation. This tutorial is a beginner’s guide to SMT. It includes an overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to obtain models and proofs. Throughout the tutorial, examples and exercises are provided as hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either thecvc5or the Z3 SMT solver. 

   more » « less