20112024

Research activity per year

Filter
Conference contribution

Search results

  • 2023

    Rely-Guarantee Reasoning for Causally Consistent Shared Memory

    Lahav, O., Dongol, B. & Wehrheim, H., 2023, Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings. Enea, C. & Lal, A. (eds.). Springer Science and Business Media Deutschland GmbH, p. 206-229 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13964 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 2022

    Abstraction for Crash-Resilient Objects

    Khyzha, A. & Lahav, O., 2022, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Sergey, I. (ed.). Springer Science and Business Media Deutschland GmbH, p. 262-289 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13240 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • An Algebraic Theory for Shared-State Concurrency

    Dvir, Y., Kammar, O. & Lahav, O., 2022, Programming Languages and Systems - 20th Asian Symposium, APLAS 2022, Proceedings. Sergey, I. (ed.). Springer Science and Business Media Deutschland GmbH, p. 3-24 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13658 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 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).

    Tel Aviv University, Bar-Ilan University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Sequential reasoning for optimizing compilers under weak memory concurrency

    Cho, M., Lee, S. H., Lee, D., Hur, C. K. & Lahav, O., 9 Jun 2022, PLDI 2022 - Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Jhala, R. & Dillig, I. (eds.). p. 213-228 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • View-Based Owicki–Gries Reasoning for Persistent x86-TSO

    Bila, E. V., Dongol, B., Lahav, O., Raad, A. & Wickerson, J., 2022, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Sergey, I. (ed.). Springer Science and Business Media Deutschland GmbH, p. 234-261 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13240 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 2021

    Modular data-race-freedom guarantees in the promising semantics

    Cho, M., Lee, S. H., Hur, C. K. & Lahav, O., 18 Jun 2021, PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Freund, S. N. & Yahav, E. (eds.). p. 867-882 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2020

    Decidable verification under a causally consistent shared memory

    Lahav, O. & Boker, U., 11 Jun 2020, PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Donaldson, A. F. & Torlak, E. (eds.). p. 211-226 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Promising 2.0: Global optimizations in relaxed memory concurrency

    Lee, S. H., Cho, M., Podkopaev, A., Chakraborty, S., Hur, C. K., Lahav, O. & Vafeiadis, V., 11 Jun 2020, PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Donaldson, A. F. & Torlak, E. (eds.). p. 362-376 15 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Reconciling event structures with modern multiprocessors

    Moiseenko, E., Podkopaev, A., Lahav, O., Melkonian, O. & Vafeiadis, V., 1 Nov 2020, 34th European Conference on Object-Oriented Programming, ECOOP 2020. Hirschfeld, R. & Pape, T. (eds.). 5. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 166).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2019

    On the semantics of snapshot isolation

    Raad, A., Lahav, O. & Vafeiadis, V., 2019, Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings. Piskac, R. & Enea, C. (eds.). p. 1-23 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11388 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Robustness against release/acquire semantics

    Lahav, O. & Margalit, R., 8 Jun 2019, PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. McKinley, K. S. & Fisher, K. (eds.). p. 126-141 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 2018

    A separation logic for a promising semantics

    Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O. & Vafeiadis, V., 2018, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ahmed, A. (ed.). p. 357-384 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10801 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • A simple cut-free system for a paraconsistent logic equivalent to S5

    Avron, A. & Lahav, O., 2018, 12th Conference on "Advances in Modal Logic", AiML 2018. Bezhanishvili, G., D'Agostino, G., Metcalfe, G. & Studer, T. (eds.). p. 29-42 14 p. (Advances in Modal Logic; vol. 12).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • On parallel snapshot isolation and release/acquire consistency

    Raad, A., Lahav, O. & Vafeiadis, V., 2018, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ahmed, A. (ed.). p. 940-967 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10801 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 2017

    A promising semantics for relaxed-memory concurrency

    Kang, J., Hur, C. K., Lahav, O., Vafeiadis, V. & Dreyer, D., 1 Jan 2017, POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Gordon, A. D. & Castagna, G. (eds.). p. 175-189 15 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 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.). 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 proceedingConference contributionpeer-review

  • Promising compilation to ARMv8 POP

    Podkopaev, A., Lahav, O. & Vafeiadis, V., 1 Jun 2017, 31st European Conference on Object-Oriented Programming, ECOOP 2017. Muller, P. (ed.). p. 221-2228 2008 p. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 74).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Repairing sequential consistency in C/C++11

    Lahav, O., Vafeiadis, V., Kang, J., Hur, C. K. & Dreyer, D., 14 Jun 2017, PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Cohen, A. & Vechev, M. (eds.). p. 618-632 15 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); vol. Part F128414).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Strong logic for weak memory: Reasoning about release-acquire consistency in iris

    Kaiser, J. O., Dang, H. H., Dreyer, D., Lahav, O. & Vafeiadis, V., 1 Jun 2017, 31st European Conference on Object-Oriented Programming, ECOOP 2017. Muller, P. (ed.). p. 171-1729 1559 p. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 74).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Verifying reachability in networks with mutable datapaths

    Panda, A., Lahav, O., Argyraki, K., Sagiv, M. & Shenker, S., 2017, Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017. p. 699-718 20 p. (Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2016

    Explaining relaxed memory models with program transformations

    Lahav, O. & Vafeiadis, V., 2016, FM 2016: Formal Methods - 21st International Symposium, Proceedings. Heitmeyer, C., Philippou, A., Gnesi, S. & Fitzgerald, J. (eds.). p. 479-495 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9995 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 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.). p. 449-468 20 p. (Advances in Modal Logic; vol. 11).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Taming release-acquire consistency

    Lahav, O., Giannarakis, N. & Vafeiadis, V., 11 Jan 2016, POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Majumdar, R. & Bodik, R. (eds.). p. 649-662 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 20-22-January-2016).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2015

    Decentralizing SDN policies

    Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M. & Shoham, S., 14 Jan 2015, POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery (ACM), p. 663-676 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 2015-January).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Owicki-Gries reasoning for weak memory models

    Lahav, O. & Vafeiadis, V., 2015, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Proceedings. Kobayashi, N., Speckmann, B., Iwama, K. & Halldorsson, M. M. (eds.). p. 311-323 13 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9135).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2014

    Modular reasoning about heap paths via effectively propositional formulas

    Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A. & Sagiv, M., 2014, POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 385-396 12 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 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. 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).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Primal infon logic with conjunctions as sets

    Cotrini, C., Gurevich, Y., Lahav, O. & Melentyev, A., 2014, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Proceedings. p. 236-249 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8705 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 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. 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).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2013

    Automated support for the investigation of paraconsistent and other logics

    Ciabattoni, A., Lahav, O., Spendier, L. & Zamansky, A., 2013, Logical Foundations of Computer Science - International Symposium, LFCS 2013, Proceedings. p. 119-133 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7734 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2012

    Effective finite-valued semantics for labelled calculi

    Baaz, M., Lahav, O. & Zamansky, A., 2012, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Proceedings. p. 52-66 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7364 LNAI).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Non-deterministic matrices for semi-canonical deduction systems

    Lahav, O., 2012, Proceedings - IEEE 42nd International Symposium on Multiple-Valued Logic, ISMVL 2012. p. 79-84 6 p. 6214787. (Proceedings of The International Symposium on Multiple-Valued Logic).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2011

    A multiple-conclusion calculus for first-order Gödel logic

    Avron, A. & Lahav, O., 2011, Computer Science - Theory and Applications - 6th International Computer Science Symposium in Russia, CSR 2011, Proceedings. p. 456-469 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6651 LNCS).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Basic constructive connectives, determinism and matrix-based semantics

    Ciabattoni, A., Lahav, O. & Zamansky, A., 2011, Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. p. 119-133 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6793 LNAI).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Kripke semantics for basic sequent systems

    Avron, A. & Lahav, O., 2011, Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. p. 43-57 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6793 LNAI).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • Non-deterministic Connectives in Propositional Gödel Logic

    Lahav, O. & Avron, A., 2011, Proceedings of the 7th Conference of the European Society for Fuzzy Logic and Technology, EUSFLAT 2011 and French Days on Fuzzy Logic and Applications, LFA 2011. 1 ed. p. 175-182 8 p. (Proceedings of the 7th Conference of the European Society for Fuzzy Logic and Technology, EUSFLAT 2011 and French Days on Fuzzy Logic and Applications, LFA 2011; vol. 1, no. 1).

    Tel Aviv University

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review