Ori Lahav

107 papers A* 11A 12B 10C 1Misc 3Journal 52Unranked 14
YearRankTypeTitle / Venue / Authors
2026 — conf
A Programming Model for Disaggregated Memory over CXL.
ASPLOS (2)
Gal Assa, Moritz Lumme, Lucas Bürgi, Michal Friedman, Ori Lahav
2026 — conf
Causal-Broadcast Memory.
ESOP (1)
Amir Karniel, Ori Lahav
2025 J jnl
A Brookes-Style Denotational Semantics for Release/Acquire Concurrency.
ACM Trans. Program. Lang. Syst.
Yotam Dvir, Ohad Kammar, Ori Lahav
2025 J jnl
Dynamic Robustness Verification Against Weak Memory (Extended Version).
CoRR
Roy David Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav
2025 J jnl
Dynamic Robustness Verification against Weak Memory.
Proc. ACM Program. Lang.
Roy David Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav
2025 — conf
Sufficient Conditions for Robustness of RDMA Programs.
ESOP (1)
Guillaume Ambal, Ori Lahav, Azalea Raad
2025 B conf
Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics.
FoSSaCS
Yotam Dvir, Ohad Kammar, Ori Lahav, Gordon D. Plotkin
2025 J jnl
Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics.
CoRR
Yotam Dvir, Ohad Kammar, Ori Lahav, Gordon D. Plotkin
2024 — conf
A Denotational Approach to Release/Acquire Concurrency.
ESOP (2)
Yotam Dvir, Ohad Kammar, Ori Lahav
2024 J jnl
A Programming Model for Disaggregated Memory over CXL.
CoRR
Gal Assa, Michal Friedman, Ori Lahav
2024 — ch.
A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal Consistency.
The Practice of Formal Methods (I)
Brijesh Dongol, Ori Lahav, Heike Wehrheim
2024 — conf
Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency.
ESOP (2)
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
2024 J jnl
Compositional Semantics for Shared-Variable Concurrency.
Proc. ACM Program. Lang.
Mikhail Svyatlovskiy, Shai Mermelstein, Ori Lahav
2024 — conf
Decidable Verification under Localized Release-Acquire Concurrency.
TACAS (3)
Abhishek Kr Singh, Ori Lahav
2024 J jnl
Extending the C/C++ Memory Model with Inline Assembly.
Proc. ACM Program. Lang.
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
2024 J jnl
Extending the C/C++ Model with Inline Assembly.
CoRR
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
2024 J jnl
Hyperproperty-Preserving Register Specifications (Extended Version).
CoRR
Yoav Ben Shimon, Ori Lahav, Sharon Shoham
2024 A conf
Hyperproperty-Preserving Register Specifications.
DISC
Yoav Ben Shimon, Ori Lahav, Sharon Shoham
2024 — conf
Intel PMDK Transactions: Specification, Validation and Concurrency.
ESOP (2)
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
2024 J jnl
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures.
Proc. ACM Program. Lang.
Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad
2024 — ed.
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I
VMCAI (1)
Rayna Dimitrova, Ori Lahav, Sebastian Wolff
2024 — ed.
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II
VMCAI (2)
Rayna Dimitrova, Ori Lahav, Sebastian Wolff
2024 A conf
What Cannot Be Implemented on Weak Memory?
DISC
Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav
2024 J jnl
What Cannot Be Implemented on Weak Memory?
CoRR
Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav
2023 J jnl
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency.
Proc. ACM Program. Lang.
Abhishek Kr Singh, Ori Lahav
2023 J jnl
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412).
Dagstuhl Reports
Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev
2023 J jnl
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version).
CoRR
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
2023 J jnl
Kater: Automating Weak Memory Model Metatheory and Consistency Checking.
Proc. ACM Program. Lang.
Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
2023 J jnl
Putting Weak Memory in Order via a Promising Intermediate Representation.
Proc. ACM Program. Lang.
Sung-Hwan Lee, Minki Cho, Roy David Margalit, Chung-Kil Hur, Ori Lahav
2023 J jnl
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version).
CoRR
Ori Lahav, Brijesh Dongol, Heike Wehrheim
2023 — conf
Rely-Guarantee Reasoning for Causally Consistent Shared Memory.
CAV (1)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
2022 A conf
Abstraction for Crash-Resilient Objects.
ESOP
Artem Khyzha, Ori Lahav
2022 B conf
An Algebraic Theory for Shared-State Concurrency.
APLAS
Yotam Dvir, Ohad Kammar, Ori Lahav
2022 A conf
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices.
IJCAR
Ori Lahav, Yoni Zohar
2022 A* conf
Sequential reasoning for optimizing compilers under weak memory concurrency.
PLDI
Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
2022 J jnl
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version).
CoRR
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
2022 A conf
View-Based Owicki-Gries Reasoning for Persistent x86-TSO.
ESOP
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
2022 J jnl
What's Decidable About Causally Consistent Shared Memory?
ACM Trans. Program. Lang. Syst.
Ori Lahav, Udi Boker
2021 J jnl
Abstraction for Crash-Resilient Objects (Extended Version).
CoRR
Artem Khyzha, Ori Lahav
2021 J jnl
Foundations of Persistent Programming (Dagstuhl Seminar 21462).
Dagstuhl Reports
Hans-Juergen Boehm, Ori Lahav, Azalea Raad
2021 J jnl
Making weak memory models fair.
Proc. ACM Program. Lang.
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
2021 A* conf
Modular data-race-freedom guarantees in the promising semantics.
PLDI
Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav
2021 J jnl
Taming x86-TSO persistency.
Proc. ACM Program. Lang.
Artem Khyzha, Ori Lahav
2021 J jnl
Verifying observational robustness against a c11-style memory model.
Proc. ACM Program. Lang.
Roy David Margalit, Ori Lahav
2020 A* conf
Decidable verification under a causally consistent shared memory.
PLDI
Ori Lahav, Udi Boker
2020 J jnl
Making Weak Memory Models Fair.
CoRR
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
2020 J jnl
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86.
Proc. ACM Program. Lang.
Azalea Raad, Ori Lahav, Viktor Vafeiadis
2020 A* conf
Promising 2.0: global optimizations in relaxed memory concurrency.
PLDI
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
2020 J jnl
Reconciling Event Structures with Modern Multiprocessors (Artifact).
Dagstuhl Artifacts Ser.
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
2020 A conf
Reconciling Event Structures with Modern Multiprocessors.
ECOOP
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
2020 J jnl
Taming x86-TSO Persistency (Extended Version).
CoRR
Artem Khyzha, Ori Lahav
2019 J jnl
Bridging the gap between programming languages and hardware weak memory models.
Proc. ACM Program. Lang.
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
2019 J jnl
Correction to: Sequent Systems for Negative Modalities.
Logica Universalis
Ori Lahav, João Marcos, Yoni Zohar
2019 J jnl
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models.
Proc. ACM Program. Lang.
Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, Viktor Vafeiadis
2019 B conf
On the Semantics of Snapshot Isolation.
VMCAI
Azalea Raad, Ori Lahav, Viktor Vafeiadis
2019 J jnl
Pure Sequent Calculi: Analyticity and Decision Procedure.
ACM Trans. Comput. Log.
Ori Lahav, Yoni Zohar
2019 J jnl
Reconciling Event Structures with Modern Multiprocessors.
CoRR
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
2019 A* conf
Robustness against release/acquire semantics.
PLDI
Ori Lahav, Roy David Margalit
2019 J jnl
Verification under causally consistent shared memory.
ACM SIGLOG News
Ori Lahav
2018 A conf
A Separation Logic for a Promising Semantics.
ESOP
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
2018 B conf
A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5.
Advances in Modal Logic
Arnon Avron, Ori Lahav
2018 J jnl
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models.
CoRR
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
2018 J jnl
Effective stateless model checking for C/C++ concurrency.
Proc. ACM Program. Lang.
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
2018 J jnl
From the subformula property to cut-admissibility in propositional sequent calculi.
J. Log. Comput.
Ori Lahav, Yoni Zohar
2018 A conf
On Parallel Snapshot Isolation and Release/Acquire Consistency.
ESOP
Azalea Raad, Ori Lahav, Viktor Vafeiadis
2018 J jnl
On the Semantics of Snapshot Isolation.
CoRR
Azalea Raad, Ori Lahav, Viktor Vafeiadis
2017 A* conf
A promising semantics for relaxed-memory concurrency.
POPL
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
2017 B conf
Cut-Admissibility as a Corollary of the Subformula Property.
TABLEAUX
Ori Lahav, Yoni Zohar
2017 A conf
Promising Compilation to ARMv8 POP.
ECOOP
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
2017 A* conf
Repairing sequential consistency in C/C++11.
PLDI
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
2017 J jnl
Sequent Systems for Negative Modalities.
Logica Universalis
Ori Lahav, João Marcos, Yoni Zohar
2017 J jnl
Sequent systems for negative modalities.
CoRR
Ori Lahav, João Marcos, Yoni Zohar
2017 J jnl
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact).
Dagstuhl Artifacts Ser.
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
2017 A conf
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.
ECOOP
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
2017 Misc conf
Verifying Reachability in Networks with Mutable Datapaths.
NSDI
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
2016 B conf
Explaining Relaxed Memory Models with Program Transformations.
FM
Ori Lahav, Viktor Vafeiadis
2016 B conf
It ain't necessarily so: Basic sequent systems for negative modalities.
Advances in Modal Logic
Ori Lahav, João Marcos, Yoni Zohar
2016 J jnl
It ain't necessarily so: Basic sequent systems for negative modalities.
CoRR
Ori Lahav, João Marcos, Yoni Zohar
2016 J jnl
Semantic investigation of canonical Gödel hypersequent systems.
J. Log. Comput.
Ori Lahav
2016 A* conf
Taming release-acquire consistency.
POPL
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
2016 J jnl
Verifying Reachability in Networks with Mutable Datapaths.
CoRR
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
2015 J jnl
A cut-free calculus for second-order Gödel logic.
Fuzzy Sets Syst.
Ori Lahav, Arnon Avron
2015 A* conf
Decentralizing SDN Policies.
POPL
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
2015 — conf
Owicki-Gries Reasoning for Weak Memory Models.
ICALP (2)
Ori Lahav, Viktor Vafeiadis
2014 A* conf
Modular reasoning about heap paths via effectively propositional formulas.
POPL
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
2014 C conf
On the Construction of Analytic Sequent Calculi for Sub-classical Logics.
WoLLIC
Ori Lahav, Yoni Zohar
2014 — conf
Primal Infon Logic with Conjunctions as Sets.
IFIP TCS
Carlos Cotrini, Yuri Gurevich, Ori Lahav, Artem Melentyev
2014 A conf
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi.
IJCAR
Ori Lahav, Yoni Zohar
2014 — —
Semantic investigation of proof systems for non-classical logics
Ori Lahav
2014 J jnl
Taming Paraconsistent (and Other) Logics: An Algorithmic Approach.
ACM Trans. Comput. Log.
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
2014 J jnl
Verifying Isolation Properties in the Presence of Middleboxes.
CoRR
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
2013 J jnl
A semantic proof of strong cut-admissibility for first-order Gödel logic.
J. Log. Comput.
Ori Lahav, Arnon Avron
2013 J jnl
A unified semantic framework for fully structural propositional sequent systems.
ACM Trans. Comput. Log.
Ori Lahav, Arnon Avron
2013 Misc conf
Automated Support for the Investigation of Paraconsistent and Other Logics.
LFCS
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
2013 J jnl
Finite-valued Semantics for Canonical Labelled Calculi.
J. Autom. Reason.
Matthias Baaz, Ori Lahav, Anna Zamansky
2013 A* conf
From Frame Properties to Hypersequent Rules in Modal Logics.
LICS
Ori Lahav
2013 — conf
Instantiations, Zippers and EPR Interpolation.
LPAR (short papers)
Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
2013 J jnl
Studying Sequent Systems
J. Multiple Valued Log. Soft Comput.
Ori Lahav
2012 A conf
Effective Finite-Valued Semantics for Labelled Calculi.
IJCAR
Matthias Baaz, Ori Lahav, Anna Zamansky
2012 — conf
Non-deterministic Matrices for Semi-canonical Deduction Systems.
ISMVL
Ori Lahav
2011 Misc conf
A Multiple-Conclusion Calculus for First-Order Gödel Logic.
CSR
Arnon Avron, Ori Lahav
2011 B conf
Basic Constructive Connectives, Determinism and Matrix-Based Semantics.
TABLEAUX
Agata Ciabattoni, Ori Lahav, Anna Zamansky
2011 B conf
Kripke Semantics for Basic Sequent Systems.
TABLEAUX
Arnon Avron, Ori Lahav
2011 — conf
Non-deterministic Connectives in Propositional Godel Logic.
EUSFLAT Conf.
Ori Lahav, Arnon Avron
2010 J jnl
On Constructive Connectives and Systems
Log. Methods Comput. Sci.
Arnon Avron, Ori Lahav
2010 — conf
Strict Canonical Constructive Systems.
Fields of Logic and Computation
Arnon Avron, Ori Lahav
2009 B conf
Canonical Constructive Systems.
TABLEAUX
Arnon Avron, Ori Lahav