6 citations · 15 across the 17 of their papers we have counts for
20 papers · 1 filter
Two generalizations of shininess
Guilherme V. Toledo, Yoni Zohar
Shininess is one of the main theory combination methods in Satisfiability Modulo Theories. We present two infinite families of generalizations of it: one involving a property betwe…
Automated Reasoning with Nested Datatypes
Tomer Hakak, Yoni Zohar, Andrew Reynolds +2
We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging.…
Bringing closure to theory combination properties
Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar
We consider the closure of three classical combination properties, namely, stable infiniteness, gentleness and shininess (or, equivalently for decidable theories, strong politeness…
Characterizing Sets of Theories That Can Be Disjointly Combined
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describ…
Shininess, strong politeness, and unicorns
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
Shininess and strong politeness are properties related to theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal an…
Number theory combination: natural density and SMT
Guilherme V. Toledo, Yoni Zohar
The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such…
Being polite is not enough (and other limits of theory combination)
Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar
In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and th…
Combining Combination Properties: Minimal Models
Guilherme Vicentin de Toledo, Yoni Zohar
This is a part of an ongoing research project, with the aim of finding the connections between properties related to theory combination in Satisfiability Modulo Theories. In previo…
Combining Finite Combination Properties: Finite Models and Busy Beavers
Guilherme Toledo, Yoni Zohar, Clark Barrett
This work is a part of an ongoing effort to understand the relationships between properties used in theory combination. We here focus on including two properties that are related t…
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness
Guilherme Vicentin de Toledo, Yoni Zohar, Clark Barrett
We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theor…
DNN Verification, Reachability, and the Exponential Function Problem
Omri Isac, Yoni Zohar, Clark Barrett +1
Deep neural networks (DNNs) are increasingly being deployed to perform safety-critical tasks. The opacity of DNNs, which prevents humans from reasoning about them, presents new saf…
Reasoning About Vectors using an SMT Theory of Sequences
Ying Sheng, Andres Nötzli, Andrew Reynolds +7
Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such progra…
lazybvtoint at the SMT Competition 2020
Yoni Zohar, Ahmed Irfan, Makai Mann +3
lazybvtoint is a new prototype SMT-solver, that will participate in the incremental and non-incremental tracks of the \qfbv logic.
Politeness and Stable Infiniteness: Stronger Together
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution is a separation between politeness and strong politeness, by…
Politeness for the Theory of Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable versi…
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar +2
This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vect…
DRAT-based Bit-Vector Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner +2
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 transla…
Towards Bit-Width-Independent Proofs in SMT Solvers
Aina Niemetz, Mathias Preiner, Andrew Reynolds +3
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used directly to reason about bit-vectors…
Sequent systems for negative modalities
Ori Lahav, João Marcos, Yoni Zohar
Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the rep…
It ain't necessarily so: Basic sequent systems for negative modalities
Ori Lahav, João Marcos, Yoni Zohar
We look at non-classical negations and their corresponding adjustment connectives from a modal viewpoint, over complete distributive lattices, and apply a very general mechanism in…