Yoni Zohar

View Scopus Profile

Yoni Zohar

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

Research activity per year

Filter
Conference contribution

Search results

  • 2024

    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

  • 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
  • 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

  • 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
  • 2020

    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

    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

  • 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
  • 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
  • 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.