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.

My research is generously supported by an ERC Starting Grant and an ISF Grant. I am seeking highly motivated candidates for postdoc, PhD, and MSc positions. If you are interested in programming language theory, concurrency, and formal methods, feel free to contact me!

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

Contact Info

Group

Yoav Ben Shimon (PhD student co-advised by Sharon Shoham)
Yotam Dvir (PhD student co-advised by Ohad Kammar)
Matan Kalp (research assistant)
Amir Karniel (PhD student)
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 (access via Moodle for TAU students)

   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 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]

Conference Papers (including PACMPL)

Two-Sorted Algebraic Decompositions of Brookes's Shared-State Denotational Semantics
Yotam Dvir, Ohad Kammar, Ori Lahav, Gordon Plotkin
FoSSaCS 2025 (accepted)

Sufficient Conditions for Robustness of RDMA Programs
Guillaume Ambal, Ori Lahav, Azalea Raad
ESOP 2025 (accepted)

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

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]

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

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

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
Yotam received the Boaz Trakhtenbrot Centennial Scholarship for this paper
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)]

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)]

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

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

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)]

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

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]

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]

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

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]

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]

A Brookes-Style Denotational Semantics for Release/Acquire Concurrency
Yotam Dvir, Ohad Kammar, Ori Lahav
Transactions on Programming Languages and Systems (TOPLAS) 2025 (accepted) [pdf]

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]

More Talks and Tutorials

A Tutorial on Weak Memory Models in Programming Language Semantics
ACM Symposium on Principles of Distributed Computing (PODC), June 2024 [slides]

Designing a Programming Language Shared-Memory Concurrency Semantics
The Technion Computer Engineering Club (ceclub), February 2021 [slides] [talk (Hebrew)]

What's Decidable about Causally Consistent Shared Memory?
Online Worldwide Seminar on Logic and Semantics (OWLS), January 2021 [slides] [talk]

Weak Memory Concurrency in C/C++11
jug.ru: Hydra-Distributed Computing Conference, St. Petresburg, July 2019 [website] [slides] [talk]

Weak Memory Concurrency in C/C++11
Haifa::C++ Meetup, November 2017 [website] [slides]

Summer School on Weak Memory Consistency
JetBrains Research, St. Petresburg, August 2017 [website] [material]

SAT-Based Decision Procedure for Analytic Sequent Calculi
Microsoft Research, Redmond, October 2013 [slides] [talk]

Semantic Investigation of Canonical Gödel Hypersequent Systems
Logic: Between Semantics and Proof Theory
A Workshop in Honor of Prof. Arnon Avron's 60th Birthday, Tel-Aviv, November 2012 [slides]

Studying Sequent Systems via Non-deterministic Many-Valued Matrices
Eighth International Tbilisi Summer School in Logic and Language, Tbilisi, September 2012 [slides]

(Non-deterministic) Semantics as a Tool for Analyzing Proof Systems
Researcher's Seminar of the Theory and Logic Group, Vienna University of Technology, April 2012 [slides]

Ori Lahav / אורי להב

Contact Info

Group

Alumni

Teaching (access via Moodle for TAU students)

Publications [dblp] [google scholar] [orcid]

Conference Papers (including PACMPL)

Abstract Presentations in International Conferences and Workshops

Theses

More Talks and Tutorials

Event Organization