Yoni Zohar

According to our database, Yoni Zohar authored at least 48 papers between 2014 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Combining Combination Properties: Minimal Models.

Guilherme Vicentin de Toledo, Yoni Zohar

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems.

Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett

Proceedings of the Formal Methods - 26th International Symposium, 2024

Satisfiability Modulo Theories: A Beginner's Tutorial.

Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar

Proceedings of the Formal Methods - 26th International Symposium, 2024

Scalable Bit-Blasting with Abstractions.

Aina Niemetz, Mathias Preiner, Yoni Zohar

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Combining Stable Infiniteness and (Strong) Politeness.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., December, 2023

Generating and Exploiting Automated Reasoning Proof Certificates.

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

Commun. ACM, October, 2023

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., September, 2023

Combining Finite Combination Properties: Finite Models and Busy Beavers.

Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Formal Verification of Bit-Vector Invertibility Conditions in Coq.

Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

DNN Verification, Reachability, and the Exponential Function Problem.

Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz

Proceedings of the 34th International Conference on Concurrency Theory, 2023

Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness.

Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Polite Combination of Algebraic Datatypes.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett

J. Autom. Reason., 2022

Bit-Precise Reasoning via Int-Blasting.

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

cvc5: A Versatile and Industrial-Strength SMT Solver.

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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices.

Ori Lahav, Yoni Zohar

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

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

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Towards Satisfiability Modulo Parametric Bit-vectors.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., 2021

lazybvtoint at the SMT Competition 2020.

Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett

CoRR, 2021

Smt-Switch: A Solver-Agnostic C++ API for SMT Solving.

Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Politeness for the Theory of Algebraic Datatypes (Extended Abstract).

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Politeness and Stable Infiniteness: Stronger Together.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic.

Norihiro Kamide, Yoni Zohar

Stud Logica, 2020

Resources: A Safe Language Abstraction for Money.

Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar

CoRR, 2020

Modal extension of ideal paraconsistent four-valued logic and its subsystem.

Norihiro Kamide, Yoni Zohar

Ann. Pure Appl. Log., 2020

The Move Prover.

Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Politeness for the Theory of Algebraic Datatypes.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Pure Sequent Calculi: Analyticity and Decision Procedure.

Ori Lahav, Yoni Zohar

ACM Trans. Comput. Log., 2019

Rexpansions of Nondeterministic matrices and their Applications in nonclassical Logics.

Arnon Avron, Yoni Zohar

Rev. Symb. Log., 2019

Correction to: Sequent Systems for Negative Modalities.

Ori Lahav, João Marcos, Yoni Zohar

Logica Universalis, 2019

Towards automated reasoning in Herbrand structures.

Liron Cohen, Reuben N. S. Rowe, Yoni Zohar

J. Log. Comput., 2019

Yet another paradefinite logic: The role of conflation1.

Norihiro Kamide, Yoni Zohar

Log. J. IGPL, 2019

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).

Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

DRAT-based Bit-Vector Proofs in CVC4.

Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Finite Model Property for Modal Ideal Paraconsistent Four-Valued Logic.

Norihiro Kamide, Yoni Zohar

Proceedings of the 2019 IEEE 49th International Symposium on Multiple-Valued Logic (ISMVL), 2019

Towards Bit-Width-Independent Proofs in SMT Solvers.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Deduction - CADE 27, 2019

Automating Automated Reasoning - The Case of Two Generic Automated Reasoning Tools.

Yoni Zohar, Dmitry Tishkovsky, Renate A. Schmidt, Anna Zamansky

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Online detection of effectively callback free objects with applications to smart contracts.

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

Proc. ACM Program. Lang., 2018

From the subformula property to cut-admissibility in propositional sequent calculi.

Ori Lahav, Yoni Zohar

J. Log. Comput., 2018

2017

Sequent Systems for Negative Modalities.

Ori Lahav, João Marcos, Yoni Zohar

Logica Universalis, 2017

Cut-Admissibility as a Corollary of the Subformula Property.

Ori Lahav, Yoni Zohar

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2017

Non-Deterministic Matrices in Action: Expansions, Refinements, and Rexpansions.

Arnon Avron, Yoni Zohar

Proceedings of the 47th IEEE International Symposium on Multiple-Valued Logic, 2017

Reasoning Inside The Box: Deduction in Herbrand Logics.

Liron Cohen, Yoni Zohar

Proceedings of the GCAI 2017, 2017

2016

'Mathematical' Does Not Mean 'Boring': Integrating Software Assignments to Enhance Learning of Logico-Mathematical Concepts.

Anna Zamansky, Yoni Zohar

Proceedings of the Advanced Information Systems Engineering Workshops, 2016

Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi.

Yoni Zohar, Anna Zamansky

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

It ain't necessarily so: Basic sequent systems for negative modalities.

Ori Lahav, João Marcos, Yoni Zohar

Proceedings of the Advances in Modal Logic 11, 2016

2014

On the Construction of Analytic Sequent Calculi for Sub-classical Logics.

Ori Lahav, Yoni Zohar

Proceedings of the Logic, Language, Information, and Computation, 2014

SAT-Based Decision Procedure for Analytic Pure Sequent Calculi.

Ori Lahav, Yoni Zohar

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014