Ori Lahav's Homepage

    

           

I am a postdoctoral researcher at MPI-SWS, working with Viktor Vafeiadis and Derek Dreyer.

I am a member of the ERC RustBelt project.

I completed my PhD at Tel Aviv University under the supervision of Arnon Avron.

 

Contact Info

See MPI-SWS page

 

 

Teaching in TAU

Computational Models: fall 08, fall 09, fall 10, spring 10, spring 11

Discrete Math: fall 11, fall 12, spring 12

 

 

Publications

 

The links on the left side are pre-copy-editing, self-produced PDFs. The definitive publisher-authenticated version is available online at the corresponding links on the right side.

Conference Papers

 

 

Repairing Sequential Consistency in C/C++11

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer

Submitted.

 

A Promising Semantics for Relaxed-Memory Concurrency

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer

Accepted to POPL 2017.

slides

Explaining Relaxed Memory Models with Program Transformations

Ori Lahav, Viktor Vafeiadis

Proceedings of FM 2016.

SpringerLink

slides

project page

It ain't necessarily so: Basic Sequent Systems for Negative Modalities

Ori Lahav, João Marcos, Yoni Zohar

Proceedings of AiML 2016.

 

Taming Release-Acquire Consistency

Ori Lahav, Nick Giannarakis, Viktor Vafeiadis

Proceedings of POPL 2016.

ACM

slides

project page

 

Owicki-Gries Reasoning for Weak Memory Models

Ori Lahav, Viktor Vafeiadis

Proceedings of ICALP 2015, track B.

SpringerLink

slides

project page

 

Decentralizing SDN Policies

Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham

Proceedings of POPL 2015.

ACM

 

Primal Infon Logic with Conjunctions as Sets

Carlos Cotrini, Yuri Gurevich, Ori Lahav, Artem Melentyev

Proceedings of TCS 2014.

SpringerLink

slides

 

On the Construction of Analytic Sequent Calculi for Sub-classical Logics

Ori Lahav, Yoni Zohar

Proceedings of WoLLIC 2014.

SpringerLink

slides

 

SAT-based Decision Procedure for Analytic Pure Sequent Calculi

Ori Lahav, Yoni Zohar

Proceedings of IJCAR 2014.

SpringerLink

slides

 

Modular Reasoning about Heap Paths via Effectively Propositional Formulas 
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv 

Proceedings of POPL 2014.

ACM

 

Instantiations, Zippers and EPR Interpolation
Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav 
Proceedings of LPAR 2013 (short paper).

EasyChair

 

From Frame Properties to Hypersequent Rules in Modal Logics

Ori Lahav

Proceedings of LICS 2013.

Kleene Award for Best Student Paper

IEEE Xplore

slides

 

Automated Support for the Investigation of Paraconsistent and Other Logics

Agata Ciabattoni,  Ori Lahav, Lara Spendier, Anna Zamansky

Proceedings of LFCS 2013.

SpringerLink

slides

 

Non-deterministic Matrices for Semi-canonical Deduction Systems

Ori Lahav

Proceedings of ISMVL 2012.

IEEE Xplore

slides

 

Effective Finite-valued Semantics for Labelled Calculi

Matthias Baaz, Ori Lahav, Anna Zamansky

Proceedings of IJCAR 2012.

SpringerLink

slides

 

Basic Constructive Connectives, Determinism and Matrix-based Semantics

Agata Ciabattoni,  Ori Lahav, Anna Zamansky

Proceedings of TABLEAUX 2011.

SpringerLink

slides

 

Kripke Semantics for Basic Sequent Systems

Arnon Avron, Ori Lahav

Proceedings of TABLEAUX 2011.

SpringerLink

slides

 

Non-deterministic Connectives in Propositional Gödel Logic

Ori Lahav, Arnon Avron

Proceedings of EUSFLAT 2011.

Atlantic Press

slides

 

A Multiple-Conclusion Calculus for First-Order Gödel Logic

Arnon Avron, Ori Lahav

Proceedings of CSR 2011.

SpringerLink

slides

 

Canonical Constructive Systems

Arnon Avron, Ori Lahav

Proceedings of TABLEAUX 2009.

SpringerLink

 

Journal Papers

 

A Cut-Free Calculus for Second-Order Gödel Logic

Ori Lahav, Arnon Avron

Fuzzy Sets and Systems (FSS), 2015.

ScienceDirect

 

Taming Paraconsistent (and Other) Logics: An Algorithmic Approach

Agata Ciabattoni,  Ori Lahav, Lara Spendier, Anna Zamansky

ACM Transactions on Computational Logic (TOCL), 2015.

ACM

 

Semantic Investigation of Canonical Gödel Hypersequent Systems

Ori Lahav

Special issue of Journal of Logic and Computation (JLC), 2016.

Oxford Journals

 

Finite-valued Semantics for Canonical Labelled Calculi

Matthias Baaz, Ori Lahav, Anna Zamansky

Journal of Automated Reasoning (JAR), 2013.

SpringerLink

 

A Unified Semantic Framework for Fully-structural Propositional Sequent Systems

Ori Lahav, Arnon Avron

ACM Transactions on Computational Logic (TOCL), 2013.

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.

Oxford Journals

 

Studying Sequent Systems via Non-deterministic Multiple-Valued Matrices

Ori Lahav

Journal of Multiple-Valued Logic and Soft Computing (MVLSC), 2013.

Old City Publishing

 

On Constructive Connectives and Systems

Arnon Avron, Ori Lahav

Logical Methods in Computer Science (LMCS), 2010.

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.

Springer Link

 

 

 

 

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.

 

 

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.

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.  

slides

 

 

Semantic Investigation of Basic Sequent Systems

Ori Lahav

Workshop on Abstract Proof Theory, Unilog 2013.

slides

 

Finite-valued Semantics for Canonical Labelled Calculi

Ori Lahav, Anna Zamansky

Compositional Meaning in Logic, GeTFun 1.0, Unilog 2013.

slides

 

Kripke-Style Semantics for Normal Systems

Arnon Avron, Ori Lahav

Second Conference of the Working Group on Mathematical Fuzzy Logic, LATD 2010.

slides

 

Invited Talks and Tutorials

SAT-Based Decision Procedure for Analytic Sequent Calculi

Microsoft Research,

Redmond, October 2013.

 

 

 

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.

 

 

 

Studying Sequent Systems via Non-deterministic Many-Valued Matrices

Eighth International Tbilisi Summer School in Logic and Language,

Tbilisi, September 2012.

 

 

 

(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.

 

 

Other Talks

Owicki-Gries for Weak Memory Models

Israeli Verification day, Tel Aviv University, 2014.

 

 

 

Theses

Ph.D Thesis, Semantic Investigation of Proof Systems for Non-classical Logics

Tel Aviv University, 2013.

slides

summary

 

 

M.Sc Thesis, Canonical Constructive Systems

Tel Aviv University, 2009.

slides

 

Tools

Paralyzer      Gen2Sat

 

 

Events

Logic: Between Semantics and Proof Theory

A Workshop in Honor of Prof. Arnon Avron's 60th Birthday

1-2 November 2012, Tel-Aviv, Israel