SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. - Ori Lahav 001; Yoni Zohar (IJCAR, 2014)

On the Construction of Analytic Sequent Calculi for Sub-classical Logics. - Ori Lahav 001; Yoni Zohar (WoLLIC, 2014)

It ain't necessarily so: Basic sequent systems for negative modalities. - Ori Lahav 001; João Marcos 001; Yoni Zohar (Advances in Modal Logic, 2016)

Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi. - Yoni Zohar; Anna Zamansky (IJCAR, 2016)

'Mathematical' Does Not Mean 'Boring': Integrating Software Assignments to Enhance Learning of Logico-Mathematical Concepts. - Anna Zamansky; Yoni Zohar (CAiSE Workshops, 2016)

Reasoning Inside The Box: Deduction in Herbrand Logics. - Liron Cohen 001; Yoni Zohar (GCAI, 2017)

Non-Deterministic Matrices in Action: Expansions, Refinements, and Rexpansions. - Arnon Avron; Yoni Zohar (ISMVL, 2017)

Cut-Admissibility as a Corollary of the Subformula Property. - Ori Lahav 001; Yoni Zohar (TABLEAUX, 2017)

Sequent Systems for Negative Modalities. - Ori Lahav 001; João Marcos 001; Yoni Zohar (Logica Universalis, 2017)

From the subformula property to cut-admissibility in propositional sequent calculi. - Ori Lahav 001; Yoni Zohar (J. Log. Comput., 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)

Automating Automated Reasoning - The Case of Two Generic Automated Reasoning Tools. - Yoni Zohar; Dmitry Tishkovsky; Renate A. Schmidt; Anna Zamansky (Description Logic, Theory Combination, and All That, 2019)

Towards Bit-Width-Independent Proofs in SMT Solvers. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (CADE, 2019)

Finite Model Property for Modal Ideal Paraconsistent Four-Valued Logic. - Norihiro Kamide; Yoni Zohar (ISMVL, 2019)

DRAT-based Bit-Vector Proofs in CVC4. - Alex Ozdemir; Aina Niemetz; Mathias Preiner; Yoni Zohar; Clark W. Barrett (SAT, 2019)

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). - Burak Ekici; Arjun Viswanathan 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (PxTP, 2019)

Yet another paradefinite logic: The role of conflation1. - Norihiro Kamide; Yoni Zohar (Log. J. IGPL, 2019)

Towards automated reasoning in Herbrand structures. - Liron Cohen 001; Reuben N. S. Rowe; Yoni Zohar (J. Log. Comput., 2019)

Correction to: Sequent Systems for Negative Modalities. - Ori Lahav 001; João Marcos 001; Yoni Zohar (Logica Universalis, 2019)

Rexpansions of Nondeterministic matrices and their Applications in nonclassical Logics. - Arnon Avron; Yoni Zohar (Rev. Symb. Log., 2019)

Pure Sequent Calculi: Analyticity and Decision Procedure. - Ori Lahav 001; Yoni Zohar (ACM Trans. Comput. Log., 2019)

Politeness for the Theory of Algebraic Datatypes. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Jane Lange; Pascal Fontaine; Clark W. Barrett (IJCAR (1), 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 (CAV (1), 2020)

Modal extension of ideal paraconsistent four-valued logic and its subsystem. - Norihiro Kamide; Yoni Zohar (Ann. Pure Appl. Log., 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)

Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic. - Norihiro Kamide; Yoni Zohar (Stud Logica, 2020)

Politeness and Stable Infiniteness: Stronger Together. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CADE, 2021)

Politeness for the Theory of Algebraic Datatypes (Extended Abstract). - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Jane Lange; Pascal Fontaine; Clark W. Barrett (IJCAI, 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 (SAT, 2021)

lazybvtoint at the SMT Competition 2020. - Yoni Zohar; Ahmed Irfan; Makai Mann; Andres Nötzli; Andrew Reynolds 001; Clark W. Barrett (CoRR, 2021)

Towards Satisfiability Modulo Parametric Bit-vectors. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2021)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. - Ori Lahav 001; Yoni Zohar (IJCAR, 2022)

Reasoning About Vectors Using an SMT Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (IJCAR, 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; et al. (TACAS (1), 2022)

Bit-Precise Reasoning via Int-Blasting. - Yoni Zohar; Ahmed Irfan; Makai Mann; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (VMCAI, 2022)

Polite Combination of Algebraic Datatypes. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Jane Lange; Pascal Fontaine; Clark W. Barrett (J. Autom. Reason., 2022)

Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. - Guilherme Vicentin de Toledo; Yoni Zohar; Clark W. Barrett (CADE, 2023)

DNN Verification, Reachability, and the Exponential Function Problem. - Omri Isac; Yoni Zohar; Clark W. Barrett; Guy Katz (CONCUR, 2023)

Formal Verification of Bit-Vector Invertibility Conditions in Coq. - Burak Ekici; Arjun Viswanathan 001; Yoni Zohar; Cesare Tinelli; Clark W. Barrett (FroCoS, 2023)

Combining Finite Combination Properties: Finite Models and Busy Beavers. - Guilherme Vicentin de Toledo; Yoni Zohar; Clark W. Barrett (FroCoS, 2023)

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 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 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

Combining Stable Infiniteness and (Strong) Politeness. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)

Scalable Bit-Blasting with Abstractions. - Aina Niemetz; Mathias Preiner; Yoni Zohar (CAV (1), 2024)

Satisfiability Modulo Theories: A Beginner's Tutorial. - Clark W. Barrett; Cesare Tinelli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar (FM (2), 2024)

The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems. - Benjamin Przybocki; Guilherme Vicentin de Toledo; Yoni Zohar; Clark W. Barrett (FM (1), 2024)

Combining Combination Properties: Minimal Models. - Guilherme Vicentin de Toledo; Yoni Zohar (LPAR, 2024)

cvc5 for SMT-COMP 2024. - Leni Aniva; Haniel Barbosa; Clark W. Barrett; Hanna Lachnitt; Daniel Larraz; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Hans-Jörg Schurr; et al. (Zenodo, 2024)

Being Polite Is Not Enough (and Other Limits of Theory Combination). - Guilherme Vicentin de Toledo; Benjamin Przybocki; Yoni Zohar (CADE, 2025)

Bit-Precise Reasoning with Parametric Bit-Vectors. - Zvika Berger; Yoni Zohar; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (SAT, 2025)

Number theory combination: natural density and SMT. - Guilherme Vicentin de Toledo; Yoni Zohar (CoRR, 2025)

Shininess, strong politeness, and unicorns. - Benjamin Przybocki; Guilherme Vicentin de Toledo; Yoni Zohar (CoRR, 2025)