Yoni Zohar

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 57

Top Topics

Sequent Calculi

Automated Reasoning

Top Venues

J. Autom. Reason.

Publications

Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems. CoRR (2024)
Guilherme Vicentin de Toledo, Yoni Zohar
Combining Combination Properties: Minimal Models. LPAR (2024)
Guilherme Vicentin de Toledo, Yoni Zohar
Combining Combination Properties: Minimal Models. CoRR (2024)
Aina Niemetz, Mathias Preiner, Yoni Zohar
Scalable Bit-Blasting with Abstractions. CAV (1) (2024)
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66 (10) (2023)
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
Combining Finite Combination Properties: Finite Models and Busy Beavers. CoRR (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67 (3) (2023)
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
Combining Finite Combination Properties: Finite Models and Busy Beavers. FroCoS (2023)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67 (4) (2023)
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
DNN Verification, Reachability, and the Exponential Function Problem. CONCUR (2023)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS (2023)
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
DNN Verification, Reachability, and the Exponential Function Problem. CoRR (2023)
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CoRR (2023)
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. CADE (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors using an SMT Theory of Sequences. CoRR (2022)
Ori Lahav, Yoni Zohar
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. IJCAR (2022)
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Bit-Precise Reasoning via Int-Blasting. VMCAI (2022)
Haniel Barbosa, Clark W. 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
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) (2022)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR (2022)
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 W. Barrett
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR (2022)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Polite Combination of Algebraic Datatypes. J. Autom. Reason. 66 (3) (2022)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Politeness and Stable Infiniteness: Stronger Together. CADE (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65 (7) (2021)
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett
lazybvtoint at the SMT Competition 2020. CoRR (2021)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI (2021)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Politeness and Stable Infiniteness: Stronger Together. CoRR (2021)
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT (2021)
Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar
Resources: A Safe Language Abstraction for Money. CoRR (2020)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Politeness for the Theory of Algebraic Datatypes. IJCAR (1) (2020)
Norihiro Kamide, Yoni Zohar
Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic. Stud Logica 108 (3) (2020)
Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill
The Move Prover. CAV (1) (2020)
Norihiro Kamide, Yoni Zohar
Modal extension of ideal paraconsistent four-valued logic and its subsystem. Ann. Pure Appl. Log. 171 (10) (2020)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Politeness for the Theory of Algebraic Datatypes. CoRR (2020)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE (2019)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP (2019)
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
DRAT-based Bit-Vector Proofs in CVC4. CoRR (2019)
Liron Cohen, Reuben N. S. Rowe, Yoni Zohar
Towards automated reasoning in Herbrand structures. J. Log. Comput. 29 (5) (2019)
Ori Lahav, João Marcos, Yoni Zohar
Correction to: Sequent Systems for Negative Modalities. Logica Universalis 13 (1) (2019)
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
DRAT-based Bit-Vector Proofs in CVC4. SAT (2019)
Norihiro Kamide, Yoni Zohar
Finite Model Property for Modal Ideal Paraconsistent Four-Valued Logic. ISMVL (2019)
Yoni Zohar, Dmitry Tishkovsky, Renate A. Schmidt, Anna Zamansky
Automating Automated Reasoning - The Case of Two Generic Automated Reasoning Tools. Description Logic, Theory Combination, and All That (2019)
Arnon Avron, Yoni Zohar
Rexpansions of Nondeterministic matrices and their Applications in nonclassical Logics. Rev. Symb. Log. 12 (1) (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR (2019)
Norihiro Kamide, Yoni Zohar
Yet another paradefinite logic: The role of conflation1. Log. J. IGPL 27 (1) (2019)
Ori Lahav, Yoni Zohar
Pure Sequent Calculi: Analyticity and Decision Procedure. ACM Trans. Comput. Log. 20 (3) (2019)
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar
Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2 (POPL) (2018)
Ori Lahav, Yoni Zohar
From the subformula property to cut-admissibility in propositional sequent calculi. J. Log. Comput. 28 (6) (2018)
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. CoRR (2018)
Ori Lahav, João Marcos, Yoni Zohar
Sequent Systems for Negative Modalities. Logica Universalis 11 (3) (2017)
Ori Lahav, João Marcos, Yoni Zohar
Sequent systems for negative modalities. CoRR (2017)
Liron Cohen, Yoni Zohar
Reasoning Inside The Box: Deduction in Herbrand Logics. GCAI (2017)
Ori Lahav, Yoni Zohar
Cut-Admissibility as a Corollary of the Subformula Property. TABLEAUX (2017)
Arnon Avron, Yoni Zohar
Non-Deterministic Matrices in Action: Expansions, Refinements, and Rexpansions. ISMVL (2017)
Anna Zamansky, Yoni Zohar
'Mathematical' Does Not Mean 'Boring': Integrating Software Assignments to Enhance Learning of Logico-Mathematical Concepts. CAiSE Workshops (2016)
Ori Lahav, João Marcos, Yoni Zohar
It ain't necessarily so: Basic sequent systems for negative modalities. Advances in Modal Logic (2016)
Yoni Zohar, Anna Zamansky
Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi. IJCAR (2016)
Ori Lahav, João Marcos, Yoni Zohar
It ain't necessarily so: Basic sequent systems for negative modalities. CoRR (2016)
Ori Lahav, Yoni Zohar
On the Construction of Analytic Sequent Calculi for Sub-classical Logics. WoLLIC (2014)
Ori Lahav, Yoni Zohar
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. IJCAR (2014)