pic

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.




pic

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!

Contact Info

Email: orilahav the letter a with a circle around it tau.ac.il
Skype: .
Office: 234 Check Point Building
Tel: +972 3 640 6422
Address: School of Computer Science, Tel Aviv University, Ramat Aviv, Tel Aviv, 6997801 Israel

Teaching

   Shared Memory Concurrency Semantics [spring 21]
   Workshop on Proof Mechanization and Program Verification in Coq [spring 23] [spring 24]
   Programming Language Foundations [spring 20] [fall 20-21] [fall 21-22] [fall 22-23] [fall 23-24]
   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) [website]

Publications [dblp] [google scholar] [orcid]

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

   Conference Papers (including PACMPL)

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

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

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

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

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]

More Talks and Tutorials

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]

Event Organization

The 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)
15-16 January 2024

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

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