More Like this

1. 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
2. Satisfiability Modulo Finite Fields

   https://doi.org/10.1007/978-3-031-37703-7_8  

   Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (January 2023, Springer Nature Switzerland)

   Enea, Constantin; Lal, Akash (Ed.)

   Abstract We study satisfiability modulo the theory of finite fields and give a decision procedure for this theory. We implement our procedure for prime fields inside the cvc5 SMT solver. Using this theory, we construct SMT queries that encode translation validation for various zero knowledge proof compilers applied to Boolean computations. We evaluate our procedure on these benchmarks. Our experiments show that our implementation is superior to previous approaches (which encode field arithmetic using integers or bit-vectors). 

   more » « less
3. Flexible Proof Production in an Industrial-Strength SMT Solver

   https://doi.org/10.1007/978-3-031-10769-6_3  

   Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Noetzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; et al (July 2022, International Joint Conference on Automated Reasoning (IJCAR))

   Blanchette, Jasmin; Kovacs, Laura; Pattinson, Dirk (Ed.)

   Proof production for SMT solvers is paramount to ensure their correctness independently from implementations, which are often prohibitively difficult to verify. Historically, however, SMT proof production has struggled with performance and coverage issues, resulting in the disabling of many crucial solving techniques and in coarse-grained (and thus hard to check) proofs. We present a flexible proof-production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers and show how we leverage it to produce detailed proofs, including for components previously unsupported by any solver. The architecture allows proofs to be produced modularly, lazily, and with numerous safeguards for correctness. This architecture has been implemented in the state-of-the-art SMT solver cvc5. We evaluate its proofs for SMT-LIB benchmarks and show that the new architecture produces better coverage than previous approaches, has acceptable performance overhead, and supports detailed proofs for most solving components. 

   more » « less
4. A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery

   Mohamed, Abdalrhman; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (October 2023, Proceedings of the 23rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23))

   Nadel, Alexander; Rozier, Kristin Yvonne (Ed.)

   Syntax-guided synthesis (SyGuS) is a recent software synthesis paradigm in which an automated synthesis tool is asked to synthesize a term that satisfies both a semantic and a syntactic specification. We consider a special case of the SyGuS problem, where a term is already known to satisfy the semantic specification but may not satisfy the syntactic one. The goal is then to find an equivalent term that additionally satisfies the syntactic specification, provided by a context-free grammar. We introduce a novel procedure for solving this problem which leverages pattern matching and automated discovery of rewrite rules. We also provide an implementation of the procedure by modifying the SyGuS solver embedded in the cvc5 SMT solver. Our evaluation shows that our new procedure significantly outperforms the state of the art on a large set of SyGuS problems for standard SMT-LIB theories such as bit-vectors, arithmetic, and strings. 

   more » « less
5. Split Gröbner Bases for Satisfiability Modulo Finite Fields

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

   Ozdemir, Alex; Pailoor, Shankara; Bassa, Alp; Ferles, Kostas; Barrett, Clark; Dillig, Işil (January 2024, Springer Nature Switzerland)

   Gurfinkel, Arie; Ganesh, Vijay (Ed.)

   Abstract Satisfiability modulo finite fields enables automated verification for cryptosystems. Unfortunately, previous solvers scale poorly for even some simple systems of field equations, in part because they build a full Gröbner basis (GB) for the system. We propose a new solver that uses multiple, simpler GBs instead of one full GB. Our solver, implemented within the cvc5 SMT solver, admits specialized propagation algorithms, e.g., for understanding bitsums. Experiments show that it solves important bitsum-heavy determinism benchmarks far faster than prior solvers, without introducing much overhead for other benchmarks. 

   more » « less