Ori Lahav / אורי להב

I am a faculty member in the School of Computer Science at Tel Aviv University. I did my PhD at Tel Aviv University under the supervision of Arnon Avron. In 2014, I was a postdoctoral researcher at Tel Aviv University hosted by Mooly Sagiv. After that, until September 2017, I was a postdoctoral researcher at MPI-SWS in Germany hosted by Viktor Vafeiadis and Derek Dreyer.

My main areas of research are programming languages and verification, with a focus on concurrency and relaxed memory models. I am also interested in proof-theory and semantics of (non-classical) logics and automated reasoning.

I am very pleased to announce that I have been awarded an ERC Starting Grant for the project "Verification-Aware Programming Language Concurrency Semantics". I am seeking highly motivated candidates for several postdoc/PhD/MSc positions. If you are interested in programming languages theory, concurrency, and formal methods, do not hesitate to contact me!

News: I gave a tutorial on "Weak Memory Models in Programming Language Semantics" at PODC'24. [slides]

Contact Info

Email: (click to reveal)
Zoom: (click to reveal)
Skype: (click to reveal)
Office: 234 Check Point Building
Tel: +972-3-640-6422
Address: School of Computer Science, Tel Aviv University, Tel Aviv, 6997801 Israel

Group

Yoav Ben Shimon (PhD student co-advised by Sharon Shoham)
Yotam Dvir (PhD student co-advised by Ohad Kammar)
Yuval Katsman Ezra (MSc student)
Roy Margalit (PhD student)
Mikhail Svyatlovskiy (research assistant)

Alumni

Ori Saporta (MSc)
Abhishek Kr Singh (postdoc, now at NUS)

Teaching

   Shared Memory Concurrency Semantics [spring 21]
   Workshop on Proof Mechanization and Program Verification in Coq [spring 23]
   Programming Language Foundations [spring 20] [fall 20-21] [fall 21-22] [fall 22-23] [fall 23-24] [fall 24-25]
   Software Foundations in Coq [spring 19]
   Concurrency Theory (undergraduate seminar) [spring 19] [spring 20] [spring 21] [spring 20] [spring 23]
   Discrete Mathematics [fall 18-19] [fall 21-22] [fall 22-23]
   Discrete Mathematics 1 [fall 23-24]
   Weakly Consistent Concurrency (graduate seminar) [spring 18]
   Advanced Seminar in Programming Languages (yearly research seminar) [calendar]

Publications [dblp] [google scholar] [orcid]

The [pdf] links include pre-copy-editing self-produced PDFs.

Conference Papers (including PACMPL)

Hyperproperty-Preserving Register Specifications
Yoav Ben Shimon, Ori Lahav, Sharon Shoham
Best Paper & Best Student Paper Awards
DISC 2024 [pdf] [full]

What Cannot Be Implemented on Weak Memory?
Armando Castañeda, Gregory Chockler, Brijesh Dongol, Ori Lahav
DISC 2024 [pdf] [full]

Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad
OOPSLA 2024 [pdf] [pdf] [project] [acm]

Extending the C/C++ Memory Model with Inline Assembly
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
OOPSLA 2024 [pdf] [full] [acm]

Compositional Semantics for Shared-Variable Concurrency
Mikhail Svyatlovskiy, Shai Mermelstein, Ori Lahav
PLDI 2024 [pdf] [full] [acm] [Coq] [slides]

A Denotational Approach to Release-Acquire Concurrency
Yotam Dvir, Ohad Kammar, Ori Lahav
ESOP 2024 [pdf] [full] [springer] [slides] [poster]

Intel PMDK Transactions: Specification and Concurrency
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, Brijesh Dongol
ESOP 2024 [pdf] [springer] [artifact report] [arxiv]

Decidable Verification under Localized Release-Acquire Concurrency
Abhishek Kr Singh, Ori Lahav
TACAS 2024 [pdf] [full] [springer] [slides] [talk (by Abhishek)]

Rely-Guarantee Reasoning for Causally Consistent Shared Memory
Ori Lahav, Brijesh Dongol, Heike Wehrheim
CAV 2023 [pdf] [full] [springer] [arxiv] [Coq]

Putting Weak Memory in Order via a Promising Intermediate Representation
Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav
PLDI 2023 [pdf] [full] [Coq (promising IR)] [Coq (mapping to ARM)] [experiments] [acm]

An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Abhishek Kr Singh, Ori Lahav
POPL 2023 [pdf] [full] [acm] [talk (by Abhishek)]

Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
POPL 2023 [pdf] [acm]

An Algebraic Theory for Shared-State Concurrency
Yotam Dvir, Ohad Kammar, Ori Lahav
APLAS 2022 [paper] [full] [springer] [slides]

Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
Ori Lahav, Yoni Zohar
IJCAR 2022 [pdf] [springer] [slides]

Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency
Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
PLDI 2022 [pdf] [full] [Coq] [acm] [talk (by Minki)]

Abstraction for Crash-Resilient Objects
Artem Khyzha, Ori Lahav
ESOP 2022 [pdf] [extended] [springer] [slides]

View-Based Owicki-Gries Reasoning for Persistent x86-TSO
Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
Distinguished Artifact Award
ESOP 2022 [pdf] [extended] [project] [Isabelle/HOL] [springer]

Making Weak Memory Models Fair
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
Distinguished Paper Award
OOPSLA 2021 [pdf] [full] [Artifact @Zenodo] [acm] [talk (by Egor)]

Modular Data-Race-Freedom Guarantees in the Promising Semantics
Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav
PLDI 2021 [pdf] [full] [Coq] [acm] [talk (by Minki)]

Taming x86-TSO Persistency
Artem Khyzha, Ori Lahav
POPL 2021 [pdf] [full] [arxiv] [acm] [talk (by Artem)]

Verifying Observational Robustness against a C11-Style Memory Model
Roy Margalit, Ori Lahav
POPL 2021 [pdf] [full] [acm] [tool] [talk (by Roy)]

Persistent Owicki-Gries Reasoning
Azalea Raad, Ori Lahav, Viktor Vafeiadis
OOPSLA 2020 [pdf] [full] [acm] [talk (by Azalea)]

Reconciling Event Structures with Modern Multiprocessors
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
ECOOP 2020 [LIPIcs] [Coq] [talk (by Evgenii)]

Decidable Verification under a Causally Consistent Shared Memory
Ori Lahav, Udi Boker
PLDI 2020 [pdf] [full] [acm] [Coq] [trailer] [talk]

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
PLDI 2020 [pdf] [full] [acm] [Coq PS2] [Coq PS2toIMM] [project page] [trailer] [talk (by Sung-Hwan)]

Robustness against Release/Acquire Semantics
Ori Lahav, Roy Margalit
PLDI 2019 [pdf] [full] [acm] [tool] [slides] [talk]

On the Semantics of Snapshot Isolation
Azalea Raad, Ori Lahav, Viktor Vafeiadis
VMCAI 2019 [pdf] [full] [springer] [arxiv] [project page]

Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
POPL 2019 [pdf] [full] [acm] [project page] [talk (by Anton)]

On Library Correctness under Weak Memory Consistency
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis
POPL 2019 [pdf] [technical appendix] [acm] [project page] [talk (by Azalea)]

A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5
Arnon Avron, Ori Lahav
AiML 2018 [pdf] [aiml]

On Parallel Snapshot Isolation and Release/Acquire Consistency
Azalea Raad, Ori Lahav, Viktor Vafeiadis
ESOP 2018 [pdf] [technical appendix] [springer] [project page]

A Separation Logic for a Promising Semantics
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
ESOP 2018 [pdf] [technical appendix] [springer]

Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
POPL 2018 [pdf] [full] [acm] [project page] [talk (by Michalis)]

Cut-Admissibility as a Corollary of the Subformula Property
Ori Lahav, Yoni Zohar
Best Paper Award
TABLEAUX 2017 [pdf] [springer]

Promising Compilation to ARMv8 POP
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
ECOOP 2017 [pdf] [full] [LIPIcs] [talk (by Anton)]

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
Best Paper Award
ECOOP 2017 [pdf] [full] [LIPIcs] [project page] [talk (by Jan-Oliver)]

Repairing Sequential Consistency in C/C++11
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
Distinguished Paper Award
PLDI 2017 [pdf] [full] [slides] [acm] [project page] [talk]

Verifying Reachability in Networks with Mutable Datapaths
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
NSDI 2017 [pdf] [usenix]

A Promising Semantics for Relaxed-Memory Concurrency
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
POPL 2017 [pdf] [full] [slides, kent concurrency workshop] [acm] [project page] [talk (by Jeehoon)]

Explaining Relaxed Memory Models with Program Transformations
Ori Lahav, Viktor Vafeiadis
FM 2016 [pdf] [slides] [springer] [project page]

It ain't necessarily so: Basic Sequent Systems for Negative Modalities
Ori Lahav, João Marcos, Yoni Zohar
AiML 2016 [pdf] [aiml]

Taming Release-Acquire Consistency
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
POPL 2016 [pdf] [full] [slides] [poster] [acm] [project page] [talk]

Owicki-Gries Reasoning for Weak Memory Models
Ori Lahav, Viktor Vafeiadis
ICALP 2015 (track B) [pdf] [full] [slides] [slides, israeli verification day 2014] [springer] [project page]

Decentralizing SDN Policies
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
POPL 2015 [pdf] [acm]

Primal Infon Logic with Conjunctions as Sets
Carlos Cotrini, Yuri Gurevich, Ori Lahav, Artem Melentyev
TCS 2014 [pdf] [slides] [springer]

On the Construction of Analytic Sequent Calculi for Sub-classical Logics
Ori Lahav, Yoni Zohar
WoLLIC 2014 [pdf] [slides] [springer]

SAT-based Decision Procedure for Analytic Pure Sequent Calculi
Ori Lahav, Yoni Zohar
IJCAR 2014 [pdf] [online tool] [slides] [springer]

Modular Reasoning about Heap Paths via Effectively Propositional Formulas
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
POPL 2014 [pdf] [acm]

Instantiations, Zippers and EPR Interpolation
Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
LPAR 2013 (short paper) [pdf] [easychair]

From Frame Properties to Hypersequent Rules in Modal Logics
Ori Lahav
Kleene Award for Best Student Paper
LICS 2013 [pdf] [slides] [acm]

Automated Support for the Investigation of Paraconsistent and Other Logics
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
LFCS 2013 [pdf] [online tool] [slides] [springer]

Non-deterministic Matrices for Semi-canonical Deduction Systems
Ori Lahav
ISMVL 2012 [pdf] [slides] [ieee]

Effective Finite-valued Semantics for Labelled Calculi
Matthias Baaz, Ori Lahav, Anna Zamansky
IJCAR 2012 [pdf] [slides] [springer]

Basic Constructive Connectives, Determinism and Matrix-based Semantics
Agata Ciabattoni, Ori Lahav, Anna Zamansky
TABLEAUX 2011 [pdf] [slides] [springer]

Kripke Semantics for Basic Sequent Systems
Arnon Avron, Ori Lahav
TABLEAUX 2011 [pdf] [slides] [springer]

Non-deterministic Connectives in Propositional Gödel Logic
Ori Lahav, Arnon Avron
EUSFLAT 2011 [pdf] [slides] [atlantic press]

A Multiple-Conclusion Calculus for First-Order Gödel Logic
Arnon Avron, Ori Lahav
CSR 2011 [pdf] [slides] [springer]

Canonical Constructive Systems
Arnon Avron, Ori Lahav
TABLEAUX 2009 [pdf] [springer]

Journal Papers

A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal Consistency
Brijesh Dongol, Ori Lahav, Heike Wehrheim
The Practice of Formal Methods, Essays in Honour of Cliff Jones 2024 [pdf] [springer]

What's Decidable about Causally Consistent Shared Memory?
Ori Lahav, Udi Boker
Transactions on Programming Languages and Systems (TOPLAS) 2022 [pdf] [acm]

Verification Under Causally Consistent Shared Memory
Ori Lahav
ACM SIGLOG News verification column April 2019 (invited) [pdf] [siglog] [acm]

Pure Sequent Calculi: Analyticity and Decision Procedure
Ori Lahav, Yoni Zohar
ACM Transactions on Computational Logic (TOCL) 2019 [pdf] [acm]

From the Subformula Property to Cut-Admissibility in Propositional Sequent Calculi
Ori Lahav, Yoni Zohar
Journal of Logic and Computation (JLC) 2018 [pdf] [oxford journals]

Sequent Systems for Negative Modalities
Ori Lahav, João Marcos, Yoni Zohar
Special Issue on "Generalizations of Truth-Functionality and Compositional Meaning in Logic"
Logica Universalis 2017 [pdf] [springer]

Semantic Investigation of Canonical Gödel Hypersequent Systems
Ori Lahav
Special Issue on "Logic: Between Semantics and Proof Theory—in Honour of Arnon Avron"
Journal of Logic and Computation (JLC) 2016 [pdf] [oxford journals]

A Cut-Free Calculus for Second-Order Gödel Logic
Ori Lahav, Arnon Avron
Fuzzy Sets and Systems 2015 [pdf] [sciencedirect]

Taming Paraconsistent (and Other) Logics: An Algorithmic Approach
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
ACM Transactions on Computational Logic 2015 [pdf] [online tool] [acm]

Finite-valued Semantics for Canonical Labelled Calculi
Matthias Baaz, Ori Lahav, Anna Zamansky
Journal of Automated Reasoning (JAR) 2013 [pdf] [springer]

A Unified Semantic Framework for Fully-structural Propositional Sequent Systems
Ori Lahav, Arnon Avron
ACM Transactions on Computational Logic (TOCL) 2013 [pdf] [acm]

A Semantic Proof of Strong Cut-admissibility for First-Order Gödel Logic
Ori Lahav, Arnon Avron
Journal of Logic and Computation (JLC) 2013 [pdf] [oxford journals]

Studying Sequent Systems via Non-deterministic Multiple-Valued Matrices
Ori Lahav
Journal of Multiple-Valued Logic and Soft Computing 2013 [pdf] [old city publishing]

On Constructive Connectives and Systems
Arnon Avron, Ori Lahav
Logical Methods in Computer Science (LMCS) 2010 [pdf] [lmcs]

Strict Canonical Constructive Systems
Arnon Avron, Ori Lahav
Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday 2010 [pdf] [springer]

Abstract Presentations in International Conferences and Workshops

A Case Against Semantic Dependencies
Ori Lahav
The Future of Weak Memory 2024, affiliated with POPL 2024 [slides]

A Denotational Approach to Release/Acquire Concurrency
Yotam Dvir, Ohad Kammar, Ori Lahav
The 15th Workshop on Games for Logic and Programming Languages, GALOP 2024, affiliated with POPL 2024 [slides]

A Monad for Shared-State Concurrency
Yotam Dvir, Ori Lahav, Ohad Kammar
The 9th ACM-SIGPLAN Workshop on Higher-Order Programming with Effects, HOPE 2021, affiliated with ICFP 2021 [slides]

Extensions of Analytic Pure Sequent Calculi with Modal Operators
Yoni Zohar, Ori Lahav
Compositional Meaning in Logic, GeTFun 4.0, affiliated with IJCAR 2016 [pdf]

A Cut-Free Calculus for Second-Order Gödel Logic
Ori Lahav, Arnon Avron
Forth Conference of the Working Group on Mathematical Fuzzy Logic, LATD 2014 [pdf] [slides]

On the Construction of Analytic Sequent Calculi for Sub-classical Logics
Ori Lahav, Yoni Zohar
Third International Workshop on "Gentzen Systems and Beyond", GSB 2014, affiliated with CSL-LICS 2014 [pdf] [slides]

Semantic Investigation of Basic Sequent Systems
Ori Lahav
Workshop on Abstract Proof Theory, Unilog 2013 [pdf] [slides]

Finite-valued Semantics for Canonical Labelled Calculi
Ori Lahav, Anna Zamansky
Compositional Meaning in Logic, GeTFun 1.0, Unilog 2013 [pdf] [slides]

Kripke-Style Semantics for Normal Systems
Arnon Avron, Ori Lahav
Second Conference of the Working Group on Mathematical Fuzzy Logic, LATD 2010 [pdf] [slides]

Theses

Semantic Investigation of Proof Systems for Non-classical Logics
Tel Aviv University, 2013 [Ph.D thesis] [slides] [summary]

Canonical Constructive Systems
Tel Aviv University, 2009 [M.Sc thesis] [slides]

Event Organization

The 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)
15-16 January 2024 [proceedings, part 1] [proceedings, part 2]

Dagstuhl Seminar: Formal Methods for Correct Persistent Programming
8-11 October 2023 [report]

SAT/SMT/AR Summer School
14-17 August 2022 (post FLoC)

Dagstuhl Seminar: Foundations of Persistent Programming
14-17 November 2021 [report]

ISRALOG17: Research Workshop of the Israel Science Foundation
15-17 October 2017, Haifa

Logic: Between Semantics and Proof Theory
A Workshop in Honor of Prof. Arnon Avron's 60th Birthday
1-2 November 2012, Tel-Aviv