Yoni Zohar

73 papers A* 1A 12B 5C 1Journal 36Unranked 16
YearRankTypeTitle / Venue / Authors
2026 J jnl
Characterizing Sets of Theories That Can Be Disjointly Combined.
Proc. ACM Program. Lang.
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar
2026 J jnl
Combining Combination Properties, Part I: Nelson-Oppen and Politeness.
J. Autom. Reason.
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2025 A conf
Being Polite Is Not Enough (and Other Limits of Theory Combination).
CADE
Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar
2025 J jnl
Being polite is not enough (and other limits of theory combination).
CoRR
Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar
2025 A conf
Bit-Precise Reasoning with Parametric Bit-Vectors.
SAT
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2025 J jnl
Characterizing Sets of Theories That Can Be Disjointly Combined.
CoRR
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar
2025 — conf
Number Theory Combination: Natural Density and SMT.
FroCoS
Guilherme Vicentin de Toledo, Yoni Zohar
2025 J jnl
Number theory combination: natural density and SMT.
CoRR
Guilherme Vicentin de Toledo, Yoni Zohar
2025 — conf
Shininess, Strong Politeness, and Unicorns.
FroCoS
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar
2025 J jnl
Shininess, strong politeness, and unicorns.
CoRR
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar
2024 B conf
Combining Combination Properties: Minimal Models.
LPAR
Guilherme Vicentin de Toledo, Yoni Zohar
2024 J jnl
Combining Combination Properties: Minimal Models.
CoRR
Guilherme Vicentin de Toledo, Yoni Zohar
2024 — ed.
Formal Methods: Foundations and Applications - 26th Brazilian Symposium, SBMF 2023, Manaus, Brazil, December 4-8, 2023, Proceedings
SBMF
Haniel Barbosa, Yoni Zohar
2024 — ed.
Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024.
SMT@CAV
Giles Reger, Yoni Zohar
2024 — conf
Satisfiability Modulo Theories: A Beginner's Tutorial.
FM (2)
Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024 — conf
Scalable Bit-Blasting with Abstractions.
CAV (1)
Aina Niemetz, Mathias Preiner, Yoni Zohar
2024 — conf
The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems.
FM (1)
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2024 J jnl
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems.
CoRR
Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023 A conf
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness.
CADE
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023 J jnl
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness.
CoRR
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023 — conf
Combining Finite Combination Properties: Finite Models and Busy Beavers.
FroCoS
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023 J jnl
Combining Finite Combination Properties: Finite Models and Busy Beavers.
CoRR
Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett
2023 J jnl
Combining Stable Infiniteness and (Strong) Politeness.
J. Autom. Reason.
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023 B conf
DNN Verification, Reachability, and the Exponential Function Problem.
CONCUR
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
2023 J jnl
DNN Verification, Reachability, and the Exponential Function Problem.
CoRR
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
2023 — conf
Formal Verification of Bit-Vector Invertibility Conditions in Coq.
FroCoS
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2023 J jnl
Generating and Exploiting Automated Reasoning Proof Certificates.
Commun. ACM
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
2023 J jnl
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.
J. Autom. Reason.
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022 B conf
Bit-Precise Reasoning via Int-Blasting.
VMCAI
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 A conf
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices.
IJCAR
Ori Lahav, Yoni Zohar
2022 A conf
Flexible Proof Production in an Industrial-Strength SMT Solver.
IJCAR
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
2022 J jnl
Polite Combination of Algebraic Datatypes.
J. Autom. Reason.
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2022 A conf
Reasoning About Vectors Using an SMT Theory of Sequences.
IJCAR
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022 J jnl
Reasoning About Vectors using an SMT Theory of Sequences.
CoRR
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022 — conf
cvc5: A Versatile and Industrial-Strength SMT Solver.
TACAS (1)
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
2021 A conf
Politeness and Stable Infiniteness: Stronger Together.
CADE
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 J jnl
Politeness and Stable Infiniteness: Stronger Together.
CoRR
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 A* conf
Politeness for the Theory of Algebraic Datatypes (Extended Abstract).
IJCAI
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2021 A conf
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving.
SAT
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett
2021 J jnl
Towards Satisfiability Modulo Parametric Bit-vectors.
J. Autom. Reason.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2021 J jnl
lazybvtoint at the SMT Competition 2020.
CoRR
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett
2020 J jnl
Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic.
Stud Logica
Norihiro Kamide, Yoni Zohar
2020 J jnl
Modal extension of ideal paraconsistent four-valued logic and its subsystem.
Ann. Pure Appl. Log.
Norihiro Kamide, Yoni Zohar
2020 — conf
Politeness for the Theory of Algebraic Datatypes.
IJCAR (1)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2020 J jnl
Politeness for the Theory of Algebraic Datatypes.
CoRR
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2020 J jnl
Resources: A Safe Language Abstraction for Money.
CoRR
Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar
2020 — conf
The Move Prover.
CAV (1)
Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill
2019 — conf
Automating Automated Reasoning - The Case of Two Generic Automated Reasoning Tools.
Description Logic, Theory Combination, and All That
Yoni Zohar, Dmitry Tishkovsky, Renate A. Schmidt, Anna Zamansky
2019 J jnl
Correction to: Sequent Systems for Negative Modalities.
Logica Universalis
Ori Lahav, João Marcos, Yoni Zohar
2019 A conf
DRAT-based Bit-Vector Proofs in CVC4.
SAT
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
2019 J jnl
DRAT-based Bit-Vector Proofs in CVC4.
CoRR
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
2019 — conf
Finite Model Property for Modal Ideal Paraconsistent Four-Valued Logic.
ISMVL
Norihiro Kamide, Yoni Zohar
2019 J jnl
Pure Sequent Calculi: Analyticity and Decision Procedure.
ACM Trans. Comput. Log.
Ori Lahav, Yoni Zohar
2019 J jnl
Rexpansions of Nondeterministic matrices and their Applications in nonclassical Logics.
Rev. Symb. Log.
Arnon Avron, Yoni Zohar
2019 A conf
Towards Bit-Width-Independent Proofs in SMT Solvers.
CADE
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Towards Bit-Width-Independent Proofs in SMT Solvers.
CoRR
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Towards automated reasoning in Herbrand structures.
J. Log. Comput.
Liron Cohen, Reuben N. S. Rowe, Yoni Zohar
2019 — conf
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).
PxTP
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Yet another paradefinite logic: The role of conflation1.
Log. J. IGPL
Norihiro Kamide, Yoni Zohar
2018 J jnl
From the subformula property to cut-admissibility in propositional sequent calculi.
J. Log. Comput.
Ori Lahav, Yoni Zohar
2018 J jnl
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts.
CoRR
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar
2018 J jnl
Online detection of effectively callback free objects with applications to smart contracts.
Proc. ACM Program. Lang.
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar
2017 B conf
Cut-Admissibility as a Corollary of the Subformula Property.
TABLEAUX
Ori Lahav, Yoni Zohar
2017 — conf
Non-Deterministic Matrices in Action: Expansions, Refinements, and Rexpansions.
ISMVL
Arnon Avron, Yoni Zohar
2017 — conf
Reasoning Inside The Box: Deduction in Herbrand Logics.
GCAI
Liron Cohen, Yoni Zohar
2017 J jnl
Sequent Systems for Negative Modalities.
Logica Universalis
Ori Lahav, João Marcos, Yoni Zohar
2017 J jnl
Sequent systems for negative modalities.
CoRR
Ori Lahav, João Marcos, Yoni Zohar
2016 — conf
'Mathematical' Does Not Mean 'Boring': Integrating Software Assignments to Enhance Learning of Logico-Mathematical Concepts.
CAiSE Workshops
Anna Zamansky, Yoni Zohar
2016 A conf
Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi.
IJCAR
Yoni Zohar, Anna Zamansky
2016 B conf
It ain't necessarily so: Basic sequent systems for negative modalities.
Advances in Modal Logic
Ori Lahav, João Marcos, Yoni Zohar
2016 J jnl
It ain't necessarily so: Basic sequent systems for negative modalities.
CoRR
Ori Lahav, João Marcos, Yoni Zohar
2014 C conf
On the Construction of Analytic Sequent Calculi for Sub-classical Logics.
WoLLIC
Ori Lahav, Yoni Zohar
2014 A conf
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi.
IJCAR
Ori Lahav, Yoni Zohar