119 citations · 152 across the 17 of their papers we have counts for
22 papers · 1 filter
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…