Canonical Constructive Systems. - Arnon Avron; Ori Lahav 001 (TABLEAUX, 2009)

Strict Canonical Constructive Systems. - Arnon Avron; Ori Lahav 001 (Fields of Logic and Computation, 2010)

On Constructive Connectives and Systems - Arnon Avron; Ori Lahav 001 (Log. Methods Comput. Sci., 2010)

A Multiple-Conclusion Calculus for First-Order Gödel Logic. - Arnon Avron; Ori Lahav 001 (CSR, 2011)

Non-deterministic Connectives in Propositional Godel Logic. - Ori Lahav 001; Arnon Avron (EUSFLAT Conf., 2011)

Kripke Semantics for Basic Sequent Systems. - Arnon Avron; Ori Lahav 001 (TABLEAUX, 2011)

Basic Constructive Connectives, Determinism and Matrix-Based Semantics. - Agata Ciabattoni; Ori Lahav 001; Anna Zamansky (TABLEAUX, 2011)

Effective Finite-Valued Semantics for Labelled Calculi. - Matthias Baaz; Ori Lahav 001; Anna Zamansky (IJCAR, 2012)

Non-deterministic Matrices for Semi-canonical Deduction Systems. - Ori Lahav 001 (ISMVL, 2012)

Automated Support for the Investigation of Paraconsistent and Other Logics. - Agata Ciabattoni; Ori Lahav 001; Lara Spendier; Anna Zamansky (LFCS, 2013)

From Frame Properties to Hypersequent Rules in Modal Logics. - Ori Lahav 001 (LICS, 2013)

Instantiations, Zippers and EPR Interpolation. - Nikolaj S. Bjørner; Arie Gurfinkel; Konstantin Korovin; Ori Lahav 001 (LPAR (short papers), 2013)

Finite-valued Semantics for Canonical Labelled Calculi. - Matthias Baaz; Ori Lahav 001; Anna Zamansky (J. Autom. Reason., 2013)

A semantic proof of strong cut-admissibility for first-order Gödel logic. - Ori Lahav 001; Arnon Avron (J. Log. Comput., 2013)

Studying Sequent Systems via Non-deterministic Multiple-Valued Matrices. - Ori Lahav 001 (J. Multiple Valued Log. Soft Comput., 2013)

A unified semantic framework for fully structural propositional sequent systems. - Ori Lahav 001; Arnon Avron (ACM Trans. Comput. Log., 2013)

SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. - Ori Lahav 001; Yoni Zohar (IJCAR, 2014)

Primal Infon Logic with Conjunctions as Sets. - Carlos Cotrini; Yuri Gurevich; Ori Lahav 001; Artem Melentyev (IFIP TCS, 2014)

Modular reasoning about heap paths via effectively propositional formulas. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Ori Lahav 001; Aleksandar Nanevski; Mooly Sagiv (POPL, 2014)

On the Construction of Analytic Sequent Calculi for Sub-classical Logics. - Ori Lahav 001; Yoni Zohar (WoLLIC, 2014)

Verifying Isolation Properties in the Presence of Middleboxes. - Aurojit Panda; Ori Lahav 001; Katerina J. Argyraki; Mooly Sagiv; Scott Shenker (CoRR, 2014)

Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. - Agata Ciabattoni; Ori Lahav 001; Lara Spendier; Anna Zamansky (ACM Trans. Comput. Log., 2014)

Semantic investigation of proof systems for non-classical logics - Ori Lahav 001 (2014)

Owicki-Gries Reasoning for Weak Memory Models. - Ori Lahav 001; Viktor Vafeiadis (ICALP (2), 2015)

Decentralizing SDN Policies. - Oded Padon; Neil Immerman; Aleksandr Karbyshev; Ori Lahav 001; Mooly Sagiv; Sharon Shoham (POPL, 2015)

A cut-free calculus for second-order Gödel logic. - Ori Lahav 001; Arnon Avron (Fuzzy Sets Syst., 2015)

It ain't necessarily so: Basic sequent systems for negative modalities. - Ori Lahav 001; João Marcos 001; Yoni Zohar (Advances in Modal Logic, 2016)

Explaining Relaxed Memory Models with Program Transformations. - Ori Lahav 001; Viktor Vafeiadis (FM, 2016)

Taming release-acquire consistency. - Ori Lahav 001; Nick Giannarakis; Viktor Vafeiadis (POPL, 2016)

Semantic investigation of canonical Gödel hypersequent systems. - Ori Lahav 001 (J. Log. Comput., 2016)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

Promising Compilation to ARMv8 POP. - Anton Podkopaev; Ori Lahav 001; Viktor Vafeiadis (ECOOP, 2017)

Verifying Reachability in Networks with Mutable Datapaths. - Aurojit Panda; Ori Lahav 001; Katerina J. Argyraki; Mooly Sagiv; Scott Shenker (NSDI, 2017)

Repairing sequential consistency in C/C++11. - Ori Lahav 001; Viktor Vafeiadis; Jeehoon Kang; Chung-Kil Hur; Derek Dreyer (PLDI, 2017)

A promising semantics for relaxed-memory concurrency. - Jeehoon Kang; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis; Derek Dreyer (POPL, 2017)

Cut-Admissibility as a Corollary of the Subformula Property. - Ori Lahav 001; Yoni Zohar (TABLEAUX, 2017)

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). - Jan-Oliver Kaiser; Hoang-Hai Dang; Derek Dreyer; Ori Lahav 001; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2017)

Sequent Systems for Negative Modalities. - Ori Lahav 001; João Marcos 001; Yoni Zohar (Logica Universalis, 2017)

A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5. - Arnon Avron; Ori Lahav 001 (Advances in Modal Logic, 2018)

On Parallel Snapshot Isolation and Release/Acquire Consistency. - Azalea Raad; Ori Lahav 001; Viktor Vafeiadis (ESOP, 2018)

A Separation Logic for a Promising Semantics. - Kasper Svendsen; Jean Pichon-Pharabod; Marko Doko; Ori Lahav 001; Viktor Vafeiadis (ESOP, 2018)

From the subformula property to cut-admissibility in propositional sequent calculi. - Ori Lahav 001; Yoni Zohar (J. Log. Comput., 2018)

Effective stateless model checking for C/C++ concurrency. - Michalis Kokologiannakis; Ori Lahav 001; Konstantinos Sagonas; Viktor Vafeiadis (Proc. ACM Program. Lang., 2018)

Robustness against release/acquire semantics. - Ori Lahav 001; Roy David Margalit (PLDI, 2019)

On the Semantics of Snapshot Isolation. - Azalea Raad; Ori Lahav 001; Viktor Vafeiadis (VMCAI, 2019)

Correction to: Sequent Systems for Negative Modalities. - Ori Lahav 001; João Marcos 001; Yoni Zohar (Logica Universalis, 2019)

Bridging the gap between programming languages and hardware weak memory models. - Anton Podkopaev; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. - Azalea Raad; Marko Doko; Lovro Rozic; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

Verification under causally consistent shared memory. - Ori Lahav 001 (ACM SIGLOG News, 2019)

Pure Sequent Calculi: Analyticity and Decision Procedure. - Ori Lahav 001; Yoni Zohar (ACM Trans. Comput. Log., 2019)

Reconciling Event Structures with Modern Multiprocessors. - Evgenii Moiseenko; Anton Podkopaev; Ori Lahav 001; Orestis Melkonian; Viktor Vafeiadis (ECOOP, 2020)

Decidable verification under a causally consistent shared memory. - Ori Lahav 001; Udi Boker (PLDI, 2020)

Promising 2.0: global optimizations in relaxed memory concurrency. - Sung-Hwan Lee 001; Minki Cho; Anton Podkopaev; Soham Chakraborty 001; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis (PLDI, 2020)

Taming x86-TSO Persistency (Extended Version). - Artem Khyzha; Ori Lahav 001 (CoRR, 2020)

Reconciling Event Structures with Modern Multiprocessors (Artifact). - Evgenii Moiseenko; Anton Podkopaev; Ori Lahav 001; Orestis Melkonian; Viktor Vafeiadis (Dagstuhl Artifacts Ser., 2020)

Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. - Azalea Raad; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2020)

Modular data-race-freedom guarantees in the promising semantics. - Minki Cho; Sung-Hwan Lee 001; Chung-Kil Hur; Ori Lahav 001 (PLDI, 2021)

Abstraction for Crash-Resilient Objects (Extended Version). - Artem Khyzha; Ori Lahav 001 (CoRR, 2021)

Foundations of Persistent Programming (Dagstuhl Seminar 21462). - Hans-Juergen Boehm; Ori Lahav 001; Azalea Raad (Dagstuhl Reports, 2021)

Taming x86-TSO persistency. - Artem Khyzha; Ori Lahav 001 (Proc. ACM Program. Lang., 2021)

Making weak memory models fair. - Ori Lahav 001; Egor Namakonov; Jonas Oberhauser; Anton Podkopaev; Viktor Vafeiadis (Proc. ACM Program. Lang., 2021)

Verifying observational robustness against a c11-style memory model. - Roy David Margalit; Ori Lahav 001 (Proc. ACM Program. Lang., 2021)

An Algebraic Theory for Shared-State Concurrency. - Yotam Dvir; Ohad Kammar; Ori Lahav 001 (APLAS, 2022)

Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. - Ori Lahav 001; Yoni Zohar (IJCAR, 2022)

View-Based Owicki-Gries Reasoning for Persistent x86-TSO. - Eleni Vafeiadi Bila; Brijesh Dongol; Ori Lahav 001; Azalea Raad; John Wickerson (ESOP, 2022)

Abstraction for Crash-Resilient Objects. - Artem Khyzha; Ori Lahav 001 (ESOP, 2022)

Sequential reasoning for optimizing compilers under weak memory concurrency. - Minki Cho; Sung-Hwan Lee 001; Dongjae Lee; Chung-Kil Hur; Ori Lahav 001 (PLDI, 2022)

View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). - Eleni Vafeiadi Bila; Brijesh Dongol; Ori Lahav 001; Azalea Raad; John Wickerson (CoRR, 2022)

What's Decidable About Causally Consistent Shared Memory? - Ori Lahav 001; Udi Boker (ACM Trans. Program. Lang. Syst., 2022)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory. - Ori Lahav 001; Brijesh Dongol; Heike Wehrheim (CAV (1), 2023)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). - Ori Lahav 001; Brijesh Dongol; Heike Wehrheim (CoRR, 2023)

Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (CoRR, 2023)

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). - Ori Lahav 001; Azalea Raad; Joseph Tassarotti; Viktor Vafeiadis; Anton Podkopaev (Dagstuhl Reports, 2023)

Putting Weak Memory in Order via a Promising Intermediate Representation. - Sung-Hwan Lee 001; Minki Cho; Roy David Margalit; Chung-Kil Hur; Ori Lahav 001 (Proc. ACM Program. Lang., 2023)

Kater: Automating Weak Memory Model Metatheory and Consistency Checking. - Michalis Kokologiannakis; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2023)

An Operational Approach to Library Abstraction under Relaxed Memory Concurrency. - Abhishek Kr Singh; Ori Lahav 001 (Proc. ACM Program. Lang., 2023)

A Denotational Approach to Release/Acquire Concurrency. - Yotam Dvir; Ohad Kammar; Ori Lahav 001 (ESOP (2), 2024)

Intel PMDK Transactions: Specification, Validation and Concurrency. - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (ESOP (2), 2024)

Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (ESOP (2), 2024)

Decidable Verification under Localized Release-Acquire Concurrency. - Abhishek Kr Singh; Ori Lahav 001 (TACAS (3), 2024)

What Cannot Be Implemented on Weak Memory? - Armando Castañeda; Gregory V. Chockler; Brijesh Dongol; Ori Lahav 001 (DISC, 2024)

Hyperproperty-Preserving Register Specifications. - Yoav Ben Shimon; Ori Lahav 001; Sharon Shoham (DISC, 2024)

A Programming Model for Disaggregated Memory over CXL. - Gal Assa; Michal Friedman 001; Ori Lahav 001 (CoRR, 2024)

Hyperproperty-Preserving Register Specifications (Extended Version). - Yoav Ben Shimon; Ori Lahav 001; Sharon Shoham (CoRR, 2024)

Extending the C/C++ Model with Inline Assembly. - Paulo Emílio de Vilhena; Ori Lahav 001; Viktor Vafeiadis; Azalea Raad (CoRR, 2024)

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 001; Azalea Raad (Proc. ACM Program. Lang., 2024)

Compositional Semantics for Shared-Variable Concurrency. - Mikhail Svyatlovskiy; Shai Mermelstein; Ori Lahav 001 (Proc. ACM Program. Lang., 2024)

Extending the C/C++ Memory Model with Inline Assembly. - Paulo Emílio de Vilhena; Ori Lahav 001; Viktor Vafeiadis; Azalea Raad (Proc. ACM Program. Lang., 2024)

A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal Consistency. - Brijesh Dongol; Ori Lahav 001; Heike Wehrheim (The Practice of Formal Methods (I), 2024)

Sufficient Conditions for Robustness of RDMA Programs. - Guillaume Ambal; Ori Lahav 001; Azalea Raad (ESOP (1), 2025)

Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics. - Yotam Dvir; Ohad Kammar; Ori Lahav 001; Gordon D. Plotkin (FoSSaCS, 2025)

Dynamic Robustness Verification against Weak Memory. - Roy David Margalit; Michalis Kokologiannakis; Shachar Itzhaky; Ori Lahav 001 (Proc. ACM Program. Lang., 2025)

Dynamic Robustness Verification Against Weak Memory (Extended Version). - Roy David Margalit; Michalis Kokologiannakis; Shachar Itzhaky; Ori Lahav 001 (CoRR, 2025)

A Brookes-Style Denotational Semantics for Release/Acquire Concurrency. - Yotam Dvir; Ohad Kammar; Ori Lahav 001 (ACM Trans. Program. Lang. Syst., 2025)