Yoni Zohar
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
30
Venues
14
Active years
2014–2026
Best venue rank
A*
Where they publish
Papers
30 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. | Andrew Reynolds, Hans-Jrg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | Checking Regular Expressions in Cvc5 Proofs. | Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | Bringing Closure to Theory Combination Properties. | Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar |
| 2026 | WoLLIC | Two Generalizations of Shininess. | Guilherme Vicentin de Toledo, Yoni Zohar |
| 2025 | CADE | Being Polite Is Not Enough (and Other Limits of Theory Combination). | Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar |
| 2025 | SAT | Bit-Precise Reasoning with Parametric Bit-Vectors. | Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2024 | CAV | Scalable Bit-Blasting with Abstractions. | Aina Niemetz, Mathias Preiner, Yoni Zohar |
| 2024 | FM | Satisfiability Modulo Theories: A Beginner's Tutorial. | Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar |
| 2024 | FM | The Nonexistence of Unicorns and Many-Sorted Lwenheim-Skolem Theorems. | Benjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
| 2024 | LPAR | Combining Combination Properties: Minimal Models. | Guilherme Vicentin de Toledo, Yoni Zohar |
| 2023 | CADE | Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. | Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
| 2023 | CONCUR | DNN Verification, Reachability, and the Exponential Function Problem. | Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. | Ori Lahav, Yoni Zohar |
| 2022 | CADE | Reasoning About Vectors Using an SMT Theory of Sequences. | Ying Sheng, Andres Ntzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | 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 Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2022 | VMCAI | Bit-Precise Reasoning via Int-Blasting. | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Ntzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | CADE | Politeness and Stable Infiniteness: Stronger Together. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | IJCAI | Politeness for the Theory of Algebraic Datatypes (Extended Abstract). | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett |
| 2021 | SAT | 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 |
| 2020 | CADE | Politeness for the Theory of Algebraic Datatypes. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett |
| 2020 | CAV | The Move Prover. | Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill |
| 2019 | CADE | Towards Bit-Width-Independent Proofs in SMT Solvers. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
| 2019 | SAT | DRAT-based Bit-Vector Proofs in CVC4. | Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett |
| 2017 | TABLEAUX | Cut-Admissibility as a Corollary of the Subformula Property. | Ori Lahav, Yoni Zohar |
| 2016 | AiML | It ain't necessarily so: Basic sequent systems for negative modalities. | Ori Lahav, Joo Marcos, Yoni Zohar |
| 2016 | CADE | Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi. | Yoni Zohar, Anna Zamansky |
| 2016 | CaiSE | 'Mathematical' Does Not Mean 'Boring': Integrating Software Assignments to Enhance Learning of Logico-Mathematical Concepts. | Anna Zamansky, Yoni Zohar |
| 2014 | CADE | SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. | Ori Lahav, Yoni Zohar |
| 2014 | WoLLIC | On the Construction of Analytic Sequent Calculi for Sub-classical Logics. | Ori Lahav, Yoni Zohar |