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.
From 2014 to 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 looking for highly motivated students and postdocs.

Contact Info

Email: @tau.ac.il
Skype: .
Office: 221 Schreiber Building
Tel: +972 3 640 7598    Fax: +972 3 640 9357
Address: School of Computer Science, Tel Aviv University, Tel Aviv, 69978 Israel

Publications [dblp] [google scholar]

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

   Conference Papers

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]

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]

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]

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]

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] [acm] [project page]

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

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 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 2013 [pdf] [springer]

A Unified Semantic Framework for Fully-structural Propositional Sequent Systems
Ori Lahav, Arnon Avron
ACM Transactions on Computational Logic 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 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 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

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

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]

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]

Events

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