| 2026 | ASPLOS | A Programming Model for Disaggregated Memory over CXL. | Gal Assa, Moritz Lumme, Lucas Brgi, Michal Friedman, Ori Lahav |
| 2026 | ESOP | Causal-Broadcast Memory. | Amir Karniel, Ori Lahav |
| 2025 | ESOP | Sufficient Conditions for Robustness of RDMA Programs. | Guillaume Ambal, Ori Lahav, Azalea Raad |
| 2025 | FOSSACS | Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics. | Yotam Dvir, Ohad Kammar, Ori Lahav, Gordon D. Plotkin |
| 2024 | CAV | Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. | Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett |
| 2024 | ESOP | A Denotational Approach to Release/Acquire Concurrency. | Yotam Dvir, Ohad Kammar, Ori Lahav |
| 2024 | ESOP | Intel PMDK Transactions: Specification, Validation and Concurrency. | Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol |
| 2024 | ESOP | Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. | Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol |
| 2024 | TACAS | Decidable Verification under Localized Release-Acquire Concurrency. | Abhishek Kr Singh, Ori Lahav |
| 2023 | CAV | Rely-Guarantee Reasoning for Causally Consistent Shared Memory. | Ori Lahav, Brijesh Dongol, Heike Wehrheim |
| 2022 | APLAS | An Algebraic Theory for Shared-State Concurrency. | Yotam Dvir, Ohad Kammar, Ori Lahav |
| 2022 | CADE | Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. | Ori Lahav, Yoni Zohar |
| 2022 | ESOP | View-Based Owicki-Gries Reasoning for Persistent x86-TSO. | Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson |
| 2022 | ESOP | Abstraction for Crash-Resilient Objects. | Artem Khyzha, Ori Lahav |
| 2022 | PLDI | Sequential reasoning for optimizing compilers under weak memory concurrency. | Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav |
| 2021 | FMCAD | Pruning and Slicing Neural Networks using Formal Verification. | Ori Lahav, Guy Katz |
| 2021 | PLDI | Modular data-race-freedom guarantees in the promising semantics. | Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav |
| 2020 | ECOOP | Reconciling Event Structures with Modern Multiprocessors. | Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis |
| 2020 | PLDI | Decidable verification under a causally consistent shared memory. | Ori Lahav, Udi Boker |
| 2020 | PLDI | Promising 2.0: global optimizations in relaxed memory concurrency. | Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis |
| 2019 | PLDI | Robustness against release/acquire semantics. | Ori Lahav, Roy David Margalit |
| 2019 | VMCAI | On the Semantics of Snapshot Isolation. | Azalea Raad, Ori Lahav, Viktor Vafeiadis |
| 2018 | AiML | A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5. | Arnon Avron, Ori Lahav |
| 2018 | ESOP | On Parallel Snapshot Isolation and Release/Acquire Consistency. | Azalea Raad, Ori Lahav, Viktor Vafeiadis |
| 2018 | ESOP | A Separation Logic for a Promising Semantics. | Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis |
| 2017 | ECOOP | Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. | Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis |
| 2017 | ECOOP | Promising Compilation to ARMv8 POP. | Anton Podkopaev, Ori Lahav, Viktor Vafeiadis |
| 2017 | NSDI | Verifying Reachability in Networks with Mutable Datapaths. | Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker |
| 2017 | PLDI | Repairing sequential consistency in C/C++11. | Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer |
| 2017 | POPL | A promising semantics for relaxed-memory concurrency. | Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer |
| 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 | FM | Explaining Relaxed Memory Models with Program Transformations. | Ori Lahav, Viktor Vafeiadis |
| 2016 | POPL | Taming release-acquire consistency. | Ori Lahav, Nick Giannarakis, Viktor Vafeiadis |
| 2015 | ICALP | Owicki-Gries Reasoning for Weak Memory Models. | Ori Lahav, Viktor Vafeiadis |
| 2015 | POPL | Decentralizing SDN Policies. | Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham |
| 2014 | CADE | SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. | Ori Lahav, Yoni Zohar |
| 2014 | POPL | Modular reasoning about heap paths via effectively propositional formulas. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2014 | WoLLIC | On the Construction of Analytic Sequent Calculi for Sub-classical Logics. | Ori Lahav, Yoni Zohar |
| 2013 | LFCS | Automated Support for the Investigation of Paraconsistent and Other Logics. | Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky |
| 2013 | LICS | From Frame Properties to Hypersequent Rules in Modal Logics. | Ori Lahav |
| 2013 | LPAR | Instantiations, Zippers and EPR Interpolation. | Nikolaj S. Bjrner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav |
| 2012 | CADE | Effective Finite-Valued Semantics for Labelled Calculi. | Matthias Baaz, Ori Lahav, Anna Zamansky |
| 2011 | CSR | A Multiple-Conclusion Calculus for First-Order Gdel Logic. | Arnon Avron, Ori Lahav |
| 2011 | EUSFLAT | Non-deterministic Connectives in Propositional Godel Logic. | Ori Lahav, Arnon Avron |
| 2011 | TABLEAUX | Kripke Semantics for Basic Sequent Systems. | Arnon Avron, Ori Lahav |
| 2011 | TABLEAUX | Basic Constructive Connectives, Determinism and Matrix-Based Semantics. | Agata Ciabattoni, Ori Lahav, Anna Zamansky |
| 2009 | TABLEAUX | Canonical Constructive Systems. | Arnon Avron, Ori Lahav |