Z3: An Efficient SMT Solver

By Leonardo de Moura, Nikolaj S. Bjørner. 2008

8,862 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Program Analysis & Verification

Citations in the corpus

Reasoning Like Program Executors (2022, methodology): “Last, we employ Z3 (De Moura and Bjørner, 2008), the well-known satisfiability modulo theory solver, as our program executor to obtain the implied result.”
Detecting Violations of Differential Privacy (2018, methodology): “The executor then uses an external MaxSMT solver such as Z3 [13] on all generated constraints to find arguments that maximizes the number of diverged branches.”
A survey of algorithmic recourse: definitions, formulations, solutions, and prospects (2020, background): “As with (M)ILP, this approach benefits from the existence of off-the-shelf solvers such as Z3 [50], CVC4 [23], and pySMT [62].”
A Survey of Symbolic Execution Techniques (2016, background): “ey make use of symbolic computation techniques only to a little extent, and their support for non-linear real and integer arithmetic is still in its infancy [1]. To the best of our knowledge, only Z3 [36] and SMT-RAT [33] can reason about them both. [1] states that using symbolic computation techniq”
MaxSMT-Based Type Inference for Python 3 (2018, methodology): “Typpete relies on Z3 [7] and the MaxRes [18] algorithm for solving the generated type constraints.”
R2: An Efficient MCMC Sampler for Probabilistic Programs (2014, methodology): “R2 is implemented in C++ and uses the Z3 theorem prover (de Moura and Bjorner 2008) in order to represent and manage preimage predicates.”
Osiris: Hunting for Integer Bugs in Ethereum Smart Contracts (2018, background): “In the case of a branch, the symbolic execution engine queries Z3 [4] in order to determine which path is feasible.”
Learning to Represent Programs with Property Signatures (2020, methodology): “We could attempt to encode the relationship between f and g into a set of formal constraints and pass that to a solver of some kind (De Moura & Bjørner, 2008), and while that is potentially an effective approach, it may be difﬁcult to scale to a language like Searcho.”
Automated Firewall Configuration in Virtual Networks (2023, neutral): “efficient in exploring the solution space [39].”
Directed Greybox Fuzzing (2017, methodology): “The constraint Π′ is passed to the Z3 Satisfiability Modulo Theory (SMT) solver [10] to compute the specific values of the identified input bytes such that bi is indeed negated.”
SecChisel Framework for Security Verification of Secure Processor Architectures (2019, methodology): “During compilation, the SecChisel code is converted to a modified FIRRTL (Flexible Intermediate Representation for RTL) [12] and then translated to logical statements that can be used with the Z3 SMT solver [9], which checks for information flow violations based on the security tags.”