Zobrazeno 1 - 10
of 114
pro vyhledávání: '"ZOHAR, YONI"'
Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are strongly finitely witnessable and smooth are called strongly polite a
Externí odkaz:
http://arxiv.org/abs/2406.18912
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 previous work, 7 properties were analyzed: convexity, stable infiniteness, s
Externí odkaz:
http://arxiv.org/abs/2405.01478
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 to shiny theories: the finite model property and stable finiteness. For
Externí odkaz:
http://arxiv.org/abs/2307.07885
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 safety and security challenges. To address these challenges, the verifica
Externí odkaz:
http://arxiv.org/abs/2305.06064
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-theoretic properties in theory combination, namely stable infiniteness, smo
Externí odkaz:
http://arxiv.org/abs/2305.02384
Autor:
Sheng, Ying, Nötzli, Andres, Reynolds, Andrew, Zohar, Yoni, Dill, David, Grieskamp, Wolfgang, Park, Junkil, Qadeer, Shaz, Barrett, Clark, Tinelli, Cesare
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 programs. The theory of arrays is widely supported but is not ideal, because
Externí odkaz:
http://arxiv.org/abs/2205.08095
lazybvtoint is a new prototype SMT-solver, that will participate in the incremental and non-incremental tracks of the \qfbv logic.
Externí odkaz:
http://arxiv.org/abs/2105.09743
Autor:
Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Reynolds, Andrew, Barrett, Clark, Tinelli, Cesare
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 presenting a polite theory that is not strongly polite. This result sh
Externí odkaz:
http://arxiv.org/abs/2104.11738
Autor:
Blackshear, Sam, Dill, David L., Qadeer, Shaz, Barrett, Clark W., Mitchell, John C., Padon, Oded, Zohar, Yoni
Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that
Externí odkaz:
http://arxiv.org/abs/2004.05106
Autor:
Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Lange, Jane, Fontaine, Pascal, Barrett, Clark
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 version, the SMT-LIB standard defines a theory of algebraic datatypes, whic
Externí odkaz:
http://arxiv.org/abs/2004.04854