Zobrazeno 1 - 10
of 35
pro vyhledávání: '"Yoni Zohar"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 301, Iss Proc. PxTP 2019, Pp 18-26 (2019)
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-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. W
Externí odkaz:
https://doaj.org/article/05aa5ad7ef454eb39cdbfc45c402d87f
Publikováno v:
Journal of Automated Reasoning
Journal of Automated Reasoning, 2022, 66 (3), pp.331-355. ⟨10.1007/s10817-022-09625-3⟩
Journal of Automated Reasoning, 2022, 66 (3), pp.331-355. ⟨10.1007/s10817-022-09625-3⟩
International audience; 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 a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8969cae924fdd0c8e251edde2ac0e8f8
https://doi.org/10.1007/s10817-022-09625-3
https://doi.org/10.1007/s10817-022-09625-3
Publikováno v:
Journal of Automated Reasoning. 65:1001-1025
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 address this shortcoming, we propose a tran
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0feba70c9ea7c21161feab14ff8198c3
https://doi.org/10.1007/s10817-021-09598-9
https://doi.org/10.1007/s10817-021-09598-9
Autor:
Yoni Zohar
Publikováno v:
Electronic Proceedings in Theoretical Computer Science. 375:1-1
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::779114de26107fddea2fd784a7a7b6e0
https://doi.org/10.4204/eptcs.375.1
https://doi.org/10.4204/eptcs.375.1
Autor:
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030945824
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::05059eddffab55cc69744b2c8a910d08
https://doi.org/10.1007/978-3-030-94583-1_24
https://doi.org/10.1007/978-3-030-94583-1_24
Autor:
Ori Lahav, Yoni Zohar
Publikováno v:
Automated Reasoning ISBN: 9783031107689
A four-valued semantics for the modal logic K is introduced. Possible worlds are replaced by a hierarchy of four-valued valuations, where the valuations of the first level correspond to valuations that are legal w.r.t. a basic non-deterministic matri
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::57427999165336eaf5f18c9e93b8adcc
https://doi.org/10.1007/978-3-031-10769-6_28
https://doi.org/10.1007/978-3-031-10769-6_28
Autor:
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett, Cesare Tinelli
Publikováno v:
Automated Reasoning ISBN: 9783031107689
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:
https://explore.openaire.eu/search/publication?articleId=doi_________::2ab2eeef98211865a6ddb880bb029e74
https://doi.org/10.1007/978-3-031-10769-6_9
https://doi.org/10.1007/978-3-031-10769-6_9
Autor:
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232
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 highlights the major features and c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ae0418867d7f4ddd7ebc064a0a8bfef9
https://doi.org/10.1007/978-3-030-99524-9_24
https://doi.org/10.1007/978-3-030-99524-9_24
Autor:
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett
Publikováno v:
Automated Reasoning ISBN: 9783031107689
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 struggled with performance and coverage i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::60d0f76591123217016b58475f230c8b
https://doi.org/10.1007/978-3-031-10769-6_3
https://doi.org/10.1007/978-3-031-10769-6_3
Publikováno v:
IJCAI 2021-International Joint Conference on Artificial Intelligence (Sister Conferences Best Papers)
IJCAI 2021-International Joint Conference on Artificial Intelligence (Sister Conferences Best Papers), Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩
IJCAI
Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21
Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21, Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩
IJCAI 2021-International Joint Conference on Artificial Intelligence (Sister Conferences Best Papers), Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩
IJCAI
Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21
Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21, Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩
International audience; 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 a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::66a28c1d101e5af0c19b26c83a3e8642
https://inria.hal.science/hal-03346697
https://inria.hal.science/hal-03346697