Yoni Zohar

View Scopus Profile

Yoni Zohar

 https://orcid.org/0000-0002-2972-6695
20142024

Research activity per year

Search results

  • 2024

    Satisfiability Modulo Theories 22nd International Workshop SMT 2024 Proceedings

    Reger, G. & Zohar, Y., 2024, In: CEUR Workshop Proceedings. 3725

    Research output: Contribution to journal › Editorial

  • Scalable Bit-Blasting with Abstractions

    Niemetz, A., Preiner, M. & Zohar, Y., 2024, Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings. Gurfinkel, A. & Ganesh, V. (eds.). Springer Science and Business Media Deutschland GmbH, p. 178-200 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14681 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
  • 2023

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

    Toledo, G. V., Zohar, Y. & Barrett, C., 2023, Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. Pientka, B. & Tinelli, C. (eds.). Springer Science and Business Media Deutschland GmbH, p. 522-541 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14132 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • Combining Finite Combination Properties: Finite Models and Busy Beavers

    Toledo, G. V., Zohar, Y. & Barrett, C., 2023, Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Proceedings. Sattler, U. & Suda, M. (eds.). Springer Science and Business Media Deutschland GmbH, p. 159-175 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14279 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • Combining Stable Infiniteness and (Strong) Politeness

    Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C. & Tinelli, C., Dec 2023, In: Journal of Automated Reasoning. 67, 4, 34.

    Research output: Contribution to journal › Article › peer-review

  • DNN Verification, Reachability, and the Exponential Function Problem

    Isac, O., Zohar, Y., Barrett, C. & Katz, G., Sep 2023, 34th International Conference on Concurrency Theory, CONCUR 2023. Perez, G. A. & Raskin, J.-F. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 26. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 279).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

  • Formal Verification of Bit-Vector Invertibility Conditions in Coq

    Ekici, B., Viswanathan, A., Zohar, Y., Tinelli, C. & Barrett, C., 2023, Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Proceedings. Sattler, U. & Suda, M. (eds.). Springer Science and Business Media Deutschland GmbH, p. 41-59 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14279 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    1 Scopus citations

  • Generating and Exploiting Automated Reasoning Proof Certificates

    Barbosa, H., Barrett, C., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C. & Zohar, Y., 22 Sep 2023, In: Communications of the ACM. 66, 10, p. 86-95 10 p.

    Research output: Contribution to journal › Article › peer-review

    3 Scopus citations

  • Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences

    Sheng, Y., Nötzli, A., Reynolds, A., Zohar, Y., Dill, D., Grieskamp, W., Park, J., Qadeer, S., Barrett, C. & Tinelli, C., Sep 2023, In: Journal of Automated Reasoning. 67, 3, 32.

    Research output: Contribution to journal › Article › peer-review

    1 Scopus citations
  • 2022

    Bit-Precise Reasoning via Int-Blasting

    Zohar, Y., Irfan, A., Mann, M., Niemetz, A., Nötzli, A., Preiner, M., Reynolds, A., Barrett, C. & Tinelli, C., 2022, Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Proceedings. Finkbeiner, B. & Wies, T. (eds.). Springer Science and Business Media Deutschland GmbH, p. 496-518 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13182 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations

  • cvc5: A Versatile and Industrial-Strength SMT Solver

    Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C. & Zohar, Y., 2022, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Fisman, D. & Rosu, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 415-442 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13243 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    147 Scopus citations

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

    Lahav, O. & Zohar, Y., 2022, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings. Blanchette, J., Kovács, L. & Pattinson, D. (eds.). Springer Science and Business Media Deutschland GmbH, p. 468-485 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13385 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    4 Scopus citations

  • Flexible Proof Production in an Industrial-Strength SMT Solver

    Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C. & Barrett, C., 2022, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings. Blanchette, J., Kovács, L. & Pattinson, D. (eds.). Springer Science and Business Media Deutschland GmbH, p. 15-35 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13385 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    13 Scopus citations

  • Polite Combination of Algebraic Datatypes

    Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P. & Barrett, C., Aug 2022, In: Journal of Automated Reasoning. 66, 3, p. 331-355 25 p.

    Research output: Contribution to journal › Article › peer-review

    Open Access
    1 Scopus citations

  • Preface

    Déharbe, D., Hyvärinen, A., Alt, L., Barbosa, H., Bjørner, N., Bonacina, M. P., Bromberger, M., Dimitrova, R., Fontaine, P., Graham-Lengrand, S., Hadarean, L., Hoenicke, J., Keller, C., Konnov, I., Marescotti, M., Niemetz, A., Polgreen, E., Preiner, M., Reynolds, A. & Schindler, T. & 4 others, Tourret, S., Zohar, Y., Schurr, H. J. & Ozdemir, A., 2022, In: CEUR Workshop Proceedings. 3185

    Research output: Contribution to journal › Editorial

  • Reasoning About Vectors Using an SMT Theory of Sequences

    Sheng, Y., Nötzli, A., Reynolds, A., Zohar, Y., Dill, D., Grieskamp, W., Park, J., Qadeer, S., Barrett, C. & Tinelli, C., 2022, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings. Blanchette, J., Kovács, L. & Pattinson, D. (eds.). Springer Science and Business Media Deutschland GmbH, p. 125-143 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13385 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    2 Scopus citations
  • 2021

    Politeness and Stable Infiniteness: Stronger Together

    Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C. & Tinelli, C., 2021, Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 148-165 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12699 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    5 Scopus citations

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

    Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P. & Barrett, C., 2021, Proceedings of the 30th International Joint Conference on Artificial Intelligence, IJCAI 2021. Zhou, Z.-H. (ed.). International Joint Conferences on Artificial Intelligence, p. 4829-4833 5 p. (IJCAI International Joint Conference on Artificial Intelligence).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

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

    Mann, M., Wilson, A., Zohar, Y., Stuntz, L., Irfan, A., Brown, K., Donovick, C., Guman, A., Tinelli, C. & Barrett, C., 2021, Theory and Applications of Satisfiability Testing – SAT 2021 - 24th International Conference, 2021, Proceedings. Li, C.-M. & Manyà, F. (eds.). Springer Science and Business Media Deutschland GmbH, p. 377-386 10 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12831 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations

  • Towards Satisfiability Modulo Parametric Bit-vectors

    Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C. & Tinelli, C., Oct 2021, In: Journal of Automated Reasoning. 65, 7, p. 1001-1025 25 p.

    Research output: Contribution to journal › Article › peer-review

    7 Scopus citations
  • 2020

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

    Kamide, N. & Zohar, Y., 1 Jun 2020, In: Studia Logica. 108, 3, p. 549-571 23 p.

    Research output: Contribution to journal › Article › peer-review

    1 Scopus citations

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

    Kamide, N. & Zohar, Y., Dec 2020, In: Annals of Pure and Applied Logic. 171, 10, 102830.

    Research output: Contribution to journal › Article › peer-review

    1 Scopus citations

  • Politeness for the Theory of Algebraic Datatypes

    Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P. & Barrett, C., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, p. 238-255 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12166 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    6 Scopus citations

  • The Move Prover

    Zhong, J. E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C. & Dill, D. L., 2020, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Lahiri, S. K. & Wang, C. (eds.). Springer, p. 137-150 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12224 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    10 Scopus citations
  • 2019

    Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools

    Zohar, Y., Tishkovsky, D., Schmidt, R. A. & Zamansky, A., 2019, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, p. 610-638 29 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11560 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

  • Correction to: Sequent Systems for Negative Modalities (Logica Universalis, (2017), 11, 3, (345-382), 10.1007/s11787-017-0175-2)

    Lahav, O., Marcos, J. & Zohar, Y., 4 Mar 2019, In: Logica Universalis. 13, 1, p. 135 1 p.

    Research output: Contribution to journal › Comment/debate

    Open Access

  • DRAT-based Bit-Vector Proofs in CVC4

    Ozdemir, A., Niemetz, A., Preiner, M., Zohar, Y. & Barrett, C., 2019, Theory and Applications of Satisfiability Testing – SAT 2019 - 22nd International Conference, SAT 2019, Proceedings. Janota, M. & Lynce, I. (eds.). Springer Verlag, p. 298-305 8 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11628 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

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

    Kamide, N. & Zohar, Y., May 2019, Proceedings - 2019 IEEE 49th International Symposium on Multiple-Valued Logic, ISMVL 2019. IEEE Computer Society, p. 120-125 6 p. 8758723. (Proceedings of The International Symposium on Multiple-Valued Logic; vol. 2019-May).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

  • Pure sequent calculi: Analyticity and decision procedure

    Lahav, O. & Zohar, Y., 2019, In: ACM Transactions on Computational Logic. 20, 3, 13.

    Research output: Contribution to journal › Article › peer-review

  • Rexpansions of nondeterministic matrices and their applications in nonclassical logics

    Avron, A. & Zohar, Y., 1 Mar 2019, In: Review of Symbolic Logic. 12, 1, p. 173-200 28 p.

    Research output: Contribution to journal › Review article › peer-review

    12 Scopus citations

  • Towards automated reasoning in Herbrand structures

    Cohen, L., Rowe, R. N. S. & Zohar, Y., 1 Sep 2019, In: Journal of Logic and Computation. 29, 5, p. 693-721 29 p.

    Research output: Contribution to journal › Article › peer-review

    Open Access
    2 Scopus citations

  • Towards bit-width-independent proofs in SMT solvers

    Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C. & Tinelli, C., 2019, Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. Fontaine, P. (ed.). Springer, p. 366-384 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11716 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    10 Scopus citations

  • Verifying bit-vector invertibility conditions in Coq – Extended abstract

    Ekici, B., Viswanathan, A., Zohar, Y., Barrett, C. & Tinelli, C., 23 Aug 2019, In: Electronic Proceedings in Theoretical Computer Science, EPTCS. 301, p. 18-26 9 p.

    Research output: Contribution to journal › Conference article › peer-review

    Open Access
    1 Scopus citations
  • 2018

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

    Lahav, O. & Zohar, Y., 5 Sep 2018, In: Journal of Logic and Computation. 28, 6, p. 1341-1366 26 p.

    Research output: Contribution to journal › Article › peer-review

    1 Scopus citations

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

    Grossman, S., Abraham, I., Golan-Gueta, G., Michalevsky, Y., Rinetzky, N., Sagiv, M. & Zohar, Y., Jan 2018, In: Proceedings of the ACM on Programming Languages. 2, POPL, 48.

    Research output: Contribution to journal › Article › peer-review

    Open Access
    122 Scopus citations
  • 2017

    Cut-admissibility as a corollary of the subformula property

    Lahav, O. & Zohar, Y., 2017, Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Proceedings. Nalon, C. & Schmidt, R. A. (eds.). Springer Verlag, p. 65-80 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10501 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

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

    Avron, A. & Zohar, Y., 30 Jun 2017, Proceedings - 2017 IEEE 47th International Symposium on Multiple-Valued Logic, ISMVL 2017. IEEE Computer Society, p. 118-123 6 p. 7964977. (Proceedings of The International Symposium on Multiple-Valued Logic).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations

  • Sequent Systems for Negative Modalities

    Lahav, O., Marcos, J. & Zohar, Y., 1 Sep 2017, In: Logica Universalis. 11, 3, p. 345-382 38 p.

    Research output: Contribution to journal › Article › peer-review

    Open Access
    9 Scopus citations
  • 2016

    Gen2sat: An automated tool for deciding derivability in analytic pure sequent calculi

    Zohar, Y. & Zamansky, A., 2016, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. Olivetti, N. & Tiwari, A. (eds.). Springer Verlag, p. 487-495 9 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9706).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations

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

    Lahav, O., Marcos, J. & Zohar, Y., 2016, Advances in Modal Logic, AiML 2016. Demri, S., Beklemishev, L. & Mate, A. (eds.). College Publications, p. 449-468 20 p. (Advances in Modal Logic; vol. 11).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations

  • ‘Mathematical’ does not mean ‘boring’: Integrating software assignments to enhance learning of logico-mathematical concepts

    Zamansky, A. & Zohar, Y., 2016, Advanced Information Systems Engineering Workshops - CAiSE 2016 International Workshops, Proceedings. Krogstie, J., Su, J. & Mouratidis, H. (eds.). Springer Verlag, p. 103-108 6 p. (Lecture Notes in Business Information Processing; vol. 249).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations
  • 2014

    On the construction of analytic sequent calculi for sub-classical logics

    Lahav, O. & Zohar, Y., 2014, Logic, Language, Information, and Computation - 21st International Workshop, WoLLIC 2014, Proceedings. Springer Verlag, p. 206-220 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8652 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    6 Scopus citations

  • SAT-Based decision procedure for analytic pure sequent calculi

    Lahav, O. & Zohar, Y., 2014, Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, p. 76-90 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8562 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    12 Scopus citations
Your message has successfully been sent.
Your message was not sent due to an error.