-
Article
Publisher Correction: Algorithm selection for SMT
-
Article
Algorithm selection for SMT
This paper presents MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language and standardized SMT-LIB theories, and is easy t...
-
Chapter and Conference Paper
Bitwuzla
Bitwuzla is a new SMT solver for the quantifier-free and quantified theories of fixed-size bit-vectors, arrays, floating-point arithmetic, and uninterpreted functions. This paper serves as a comprehensive syst...
-
Chapter and Conference Paper
Flexible Proof Production in an Industrial-Strength SMT Solver
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 ...
-
Chapter and Conference Paper
cvc5: A Versatile and Industrial-Strength SMT Solver
cvc5 is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of cvc5 ’s architectural design and...
-
Chapter and Conference Paper
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
SMT solvers are highly complex pieces of software with performance, robustness, and correctness as key requirements. Complementing traditional testing techniques for these solvers with randomized stress testin...
-
Chapter and Conference Paper
Bit-Precise Reasoning via Int-Blasting
The state of the art for bit-precise reasoning in the context of Satisfiability Modulo Theories (SMT) is a SAT-based technique called bit-blasting where the input formula is first simplified and then translate...
-
Article
Towards Satisfiability Modulo Parametric Bit-vectors
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These techniques, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To ad...
-
Article
On solving quantified bit-vector constraints using invertibility conditions
We present a novel approach for solving quantified bit-vector constraints in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precise...
-
Chapter and Conference Paper
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends
Erroneous behavior of verification back ends such as SMT solvers require effective and efficient techniques to identify, locate and fix failures of any kind. Manual analysis of large real-world inputs usually ...
-
Chapter and Conference Paper
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
In this paper, we present MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language. It employs machine learning (ML) methods ...
-
Chapter and Conference Paper
Syntax-Guided Quantifier Instantiation
This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified con...
-
Chapter and Conference Paper
DRAT-based Bit-Vector Proofs in CVC4
Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiabi...
-
Chapter and Conference Paper
Towards Bit-Width-Independent Proofs in SMT Solvers
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas
-
Chapter and Conference Paper
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
The performance of modern Satisfiability Modulo Theories (SMT) solvers relies crucially on efficient decision procedures as well as static simplification techniques, which include large sets of rewrite rules
-
Chapter and Conference Paper
Invertibility Conditions for Floating-Point Formulas
Automated reasoning procedures are essential for a number of applic...
-
Chapter and Conference Paper
Btor2 , BtorMC and Boolector 3.0
We describe Btor2, a word-level model checking format for capturing models of hardware and potentially software in a bit-precise manner. This simple, line-based and easy to parse format can be seen as a sorted ex...
-
Chapter and Conference Paper
Solving Quantified Bit-Vectors Using Invertibility Conditions
We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely ...
-
Article
Open AccessPropagation based local search for bit-precise reasoning
Many applications of computer-aided verification require bit-precise reasoning as provided by satisfiability modulo theories (SMT) solvers for the theory of quantifier-free fixed-size bit-vectors. The current ...
-
Chapter and Conference Paper
Counterexample-Guided Model Synthesis
In this paper we present a new approach for solving quantified formulas in Satisfiability Modulo Theories (SMT), with a particular focus on the theory of fixed-size bit-vectors. We combine counterexample-guide...
