default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDOri Lahav 0001
Person information
- affiliation: Tel Aviv University, Israel
Other persons with the same name
- Ori Lahav 0002 — Hebrew University of Jerusalem, Israel
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j29]Paulo Emílio de Vilhena
, Ori Lahav, Viktor Vafeiadis, Azalea Raad:
Extending the C/C++ Memory Model with Inline Assembly. Proc. ACM Program. Lang. 8(OOPSLA2): 1081-1107 (2024)- [j28]Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad:
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. Proc. ACM Program. Lang. 8(OOPSLA2): 1982-2009 (2024) - [j27]Mikhail Svyatlovskiy, Shai Mermelstein, Ori Lahav:
Compositional Semantics for Shared-Variable Concurrency. Proc. ACM Program. Lang. 8(PLDI): 543-566 (2024) - [c47]Yotam Dvir, Ohad Kammar, Ori Lahav:
A Denotational Approach to Release/Acquire Concurrency. ESOP (2) 2024: 121-149 - [c46]Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol:
Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) 2024: 150-179 - [c45]Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol:
Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. ESOP (2) 2024: 180-184 - [c44]Abhishek Kr Singh, Ori Lahav:
Decidable Verification under Localized Release-Acquire Concurrency. TACAS (3) 2024: 235-254 - [c43]Yoav Ben Shimon, Ori Lahav, Sharon Shoham:
Hyperproperty-Preserving Register Specifications. DISC 2024: 8:1-8:19 - [c42]Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav:
What Cannot Be Implemented on Weak Memory? DISC 2024: 11:1-11:22 - [e2]Rayna Dimitrova, Ori Lahav, Sebastian Wolff:
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14499, Springer 2024, ISBN 978-3-031-50523-2 [contents] - [e1]Rayna Dimitrova, Ori Lahav, Sebastian Wolff:
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14500, Springer 2024, ISBN 978-3-031-50520-1 [contents] - [i19]Armando Castañeda, Gregory V. Chockler, Brijesh Dongol, Ori Lahav:
What Cannot Be Implemented on Weak Memory? CoRR abs/2405.16611 (2024) - [i18]Gal Assa, Michal Friedman, Ori Lahav:
A Programming Model for Disaggregated Memory over CXL. CoRR abs/2407.16300 (2024) - [i17]Yoav Ben Shimon, Ori Lahav, Sharon Shoham:
Hyperproperty-Preserving Register Specifications (Extended Version). CoRR abs/2408.11015 (2024) - [i16]Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad:
Extending the C/C++ Model with Inline Assembly. CoRR abs/2408.17208 (2024) - 2023
- [j26]Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav:
Putting Weak Memory in Order via a Promising Intermediate Representation. Proc. ACM Program. Lang. 7(PLDI): 1872-1895 (2023) - [j25]Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis:
Kater: Automating Weak Memory Model Metatheory and Consistency Checking. Proc. ACM Program. Lang. 7(POPL): 544-572 (2023) - [j24]Abhishek Kr Singh, Ori Lahav:
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency. Proc. ACM Program. Lang. 7(POPL): 1542-1572 (2023) - [c41]Ori Lahav, Brijesh Dongol, Heike Wehrheim:
Rely-Guarantee Reasoning for Causally Consistent Shared Memory. CAV (1) 2023: 206-229 - [i15]Ori Lahav, Brijesh Dongol, Heike Wehrheim:
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). CoRR abs/2305.08486 (2023) - [i14]Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol:
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). CoRR abs/2312.13828 (2023) - [i13]Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev:
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). Dagstuhl Reports 13(10): 50-64 (2023) - 2022
- [j23]Ori Lahav, Udi Boker:
What's Decidable About Causally Consistent Shared Memory? ACM Trans. Program. Lang. Syst. 44(2): 8:1-8:55 (2022) - [c40]Yotam Dvir, Ohad Kammar, Ori Lahav:
An Algebraic Theory for Shared-State Concurrency. APLAS 2022: 3-24 - [c39]Ori Lahav, Yoni Zohar:
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. IJCAR 2022: 468-485 - [c38]Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson:
View-Based Owicki-Gries Reasoning for Persistent x86-TSO. ESOP 2022: 234-261 - [c37]Artem Khyzha, Ori Lahav:
Abstraction for Crash-Resilient Objects. ESOP 2022: 262-289 - [c36]Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav:
Sequential reasoning for optimizing compilers under weak memory concurrency. PLDI 2022: 213-228 - [i12]Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson:
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). CoRR abs/2201.05860 (2022) - 2021
- [j22]Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis:
Making weak memory models fair. Proc. ACM Program. Lang. 5(OOPSLA): 1-27 (2021) - [j21]Artem Khyzha, Ori Lahav:
Taming x86-TSO persistency. Proc. ACM Program. Lang. 5(POPL): 1-29 (2021) - [j20]Roy Margalit, Ori Lahav:
Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang. 5(POPL): 1-33 (2021) - [c35]Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav:
Modular data-race-freedom guarantees in the promising semantics. PLDI 2021: 867-882 - [i11]Artem Khyzha, Ori Lahav:
Abstraction for Crash-Resilient Objects (Extended Version). CoRR abs/2111.03881 (2021) - [i10]Hans-Juergen Boehm, Ori Lahav, Azalea Raad:
Foundations of Persistent Programming (Dagstuhl Seminar 21462). Dagstuhl Reports 11(10): 94-110 (2021) - 2020
- [j19]Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis:
Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Ser. 6(2): 04:1-04:3 (2020) - [j18]Azalea Raad, Ori Lahav, Viktor Vafeiadis:
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. 4(OOPSLA): 151:1-151:28 (2020) - [c34]Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis:
Reconciling Event Structures with Modern Multiprocessors. ECOOP 2020: 5:1-5:26 - [c33]Ori Lahav, Udi Boker:
Decidable verification under a causally consistent shared memory. PLDI 2020: 211-226 - [c32]Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis:
Promising 2.0: global optimizations in relaxed memory concurrency. PLDI 2020: 362-376 - [i9]Artem Khyzha, Ori Lahav:
Taming x86-TSO Persistency (Extended Version). CoRR abs/2010.13593 (2020) - [i8]Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis:
Making Weak Memory Models Fair. CoRR abs/2012.01067 (2020)
2010 – 2019
- 2019
- [j17]Ori Lahav, João Marcos, Yoni Zohar:
Correction to: Sequent Systems for Negative Modalities. Logica Universalis 13(1): 135 (2019) - [j16]Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, Viktor Vafeiadis:
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3(POPL): 68:1-68:31 (2019) - [j15]Anton Podkopaev, Ori Lahav, Viktor Vafeiadis:
Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3(POPL): 69:1-69:31 (2019) - [j14]Ori Lahav:
Verification under causally consistent shared memory. ACM SIGLOG News 6(2): 43-56 (2019) - [j13]Ori Lahav, Yoni Zohar:
Pure Sequent Calculi: Analyticity and Decision Procedure. ACM Trans. Comput. Log. 20(3): 13:1-13:38 (2019) - [c31]Ori Lahav, Roy Margalit:
Robustness against release/acquire semantics. PLDI 2019: 126-141 - [c30]Azalea Raad, Ori Lahav, Viktor Vafeiadis:
On the Semantics of Snapshot Isolation. VMCAI 2019: 1-23 - [i7]Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis:
Reconciling Event Structures with Modern Multiprocessors. CoRR abs/1911.06567 (2019) - 2018
- [j12]Ori Lahav, Yoni Zohar:
From the subformula property to cut-admissibility in propositional sequent calculi. J. Log. Comput. 28(6): 1341-1366 (2018) - [j11]Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis:
Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2(POPL): 17:1-17:32 (2018) - [c29]Arnon Avron, Ori Lahav:
A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5. Advances in Modal Logic 2018: 29-42 - [c28]Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis:
A Separation Logic for a Promising Semantics. ESOP 2018: 357-384 - [c27]Azalea Raad, Ori Lahav, Viktor Vafeiadis:
On Parallel Snapshot Isolation and Release/Acquire Consistency. ESOP 2018: 940-967 - [i6]Azalea Raad, Ori Lahav, Viktor Vafeiadis:
On the Semantics of Snapshot Isolation. CoRR abs/1805.06196 (2018) - [i5]Anton Podkopaev, Ori Lahav, Viktor Vafeiadis:
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. CoRR abs/1807.07892 (2018) - 2017
- [j10]Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis:
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). Dagstuhl Artifacts Ser. 3(2): 15:1-15:2 (2017) - [j9]Ori Lahav, João Marcos, Yoni Zohar:
Sequent Systems for Negative Modalities. Logica Universalis 11(3): 345-382 (2017) - [c26]Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis:
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. ECOOP 2017: 17:1-17:29 - [c25]Anton Podkopaev, Ori Lahav, Viktor Vafeiadis:
Promising Compilation to ARMv8 POP. ECOOP 2017: 22:1-22:28 - [c24]Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker:
Verifying Reachability in Networks with Mutable Datapaths. NSDI 2017: 699-718 - [c23]Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer:
Repairing sequential consistency in C/C++11. PLDI 2017: 618-632 - [c22]Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer:
A promising semantics for relaxed-memory concurrency. POPL 2017: 175-189 - [c21]Ori Lahav, Yoni Zohar:
Cut-Admissibility as a Corollary of the Subformula Property. TABLEAUX 2017: 65-80 - [i4]Ori Lahav, João Marcos, Yoni Zohar:
Sequent systems for negative modalities. CoRR abs/1706.05945 (2017) - 2016
- [j8]Ori Lahav:
Semantic investigation of canonical Gödel hypersequent systems. J. Log. Comput. 26(1): 337-360 (2016) - [c20]Ori Lahav, João Marcos, Yoni Zohar:
It ain't necessarily so: Basic sequent systems for negative modalities. Advances in Modal Logic 2016: 449-468 - [c19]Ori Lahav, Viktor Vafeiadis:
Explaining Relaxed Memory Models with Program Transformations. FM 2016: 479-495 - [c18]Ori Lahav, Nick Giannarakis, Viktor Vafeiadis:
Taming release-acquire consistency. POPL 2016: 649-662 - [i3]Ori Lahav, João Marcos, Yoni Zohar:
It ain't necessarily so: Basic sequent systems for negative modalities. CoRR abs/1606.04006 (2016) - [i2]Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker:
Verifying Reachability in Networks with Mutable Datapaths. CoRR abs/1607.00991 (2016) - 2015
- [j7]Ori Lahav, Arnon Avron:
A cut-free calculus for second-order Gödel logic. Fuzzy Sets Syst. 276: 1-30 (2015) - [c17]Ori Lahav, Viktor Vafeiadis:
Owicki-Gries Reasoning for Weak Memory Models. ICALP (2) 2015: 311-323 - [c16]Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham:
Decentralizing SDN Policies. POPL 2015: 663-676 - 2014
- [b1]Ori Lahav:
Semantic investigation of proof systems for non-classical logics. Tel Aviv University, Israel, 2014 - [j6]Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky:
Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. ACM Trans. Comput. Log. 16(1): 5:1-5:23 (2014) - [c15]Ori Lahav, Yoni Zohar:
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. IJCAR 2014: 76-90 - [c14]Carlos Cotrini, Yuri Gurevich, Ori Lahav, Artem Melentyev:
Primal Infon Logic with Conjunctions as Sets. IFIP TCS 2014: 236-249 - [c13]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv:
Modular reasoning about heap paths via effectively propositional formulas. POPL 2014: 385-396 - [c12]Ori Lahav, Yoni Zohar:
On the Construction of Analytic Sequent Calculi for Sub-classical Logics. WoLLIC 2014: 206-220 - [i1]Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker:
Verifying Isolation Properties in the Presence of Middleboxes. CoRR abs/1409.7687 (2014) - 2013
- [j5]Matthias Baaz, Ori Lahav, Anna Zamansky:
Finite-valued Semantics for Canonical Labelled Calculi. J. Autom. Reason. 51(4): 401-430 (2013) - [j4]Ori Lahav, Arnon Avron:
A semantic proof of strong cut-admissibility for first-order Gödel logic. J. Log. Comput. 23(1): 59-86 (2013) - [j3]Ori Lahav:
Studying Sequent Systems via Non-deterministic Multiple-Valued Matrices. J. Multiple Valued Log. Soft Comput. 21(5-6): 575-595 (2013) - [j2]Ori Lahav, Arnon Avron:
A unified semantic framework for fully structural propositional sequent systems. ACM Trans. Comput. Log. 14(4): 27:1-27:33 (2013) - [c11]Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky:
Automated Support for the Investigation of Paraconsistent and Other Logics. LFCS 2013: 119-133 - [c10]Ori Lahav:
From Frame Properties to Hypersequent Rules in Modal Logics. LICS 2013: 408-417 - [c9]Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav:
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) 2013: 35-41 - 2012
- [c8]Matthias Baaz, Ori Lahav, Anna Zamansky:
Effective Finite-Valued Semantics for Labelled Calculi. IJCAR 2012: 52-66 - [c7]Ori Lahav:
Non-deterministic Matrices for Semi-canonical Deduction Systems. ISMVL 2012: 79-84 - 2011
- [c6]Arnon Avron, Ori Lahav:
A Multiple-Conclusion Calculus for First-Order Gödel Logic. CSR 2011: 456-469 - [c5]Ori Lahav, Arnon Avron:
Non-deterministic Connectives in Propositional Godel Logic. EUSFLAT Conf. 2011: 175-182 - [c4]Arnon Avron, Ori Lahav:
Kripke Semantics for Basic Sequent Systems. TABLEAUX 2011: 43-57 - [c3]Agata Ciabattoni, Ori Lahav, Anna Zamansky:
Basic Constructive Connectives, Determinism and Matrix-Based Semantics. TABLEAUX 2011: 119-133 - 2010
- [j1]Arnon Avron, Ori Lahav:
On Constructive Connectives and Systems. Log. Methods Comput. Sci. 6(4) (2010) - [c2]Arnon Avron, Ori Lahav:
Strict Canonical Constructive Systems. Fields of Logic and Computation 2010: 75-94
2000 – 2009
- 2009
- [c1]Arnon Avron, Ori Lahav:
Canonical Constructive Systems. TABLEAUX 2009: 62-76
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 00:19 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
