Ori Lahav

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 62

Top Topics

Sequent Calculi

Snapshot Isolation

Top Venues

Proc. ACM Program. Lang.

Publications

Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CAV (2) (2024)
Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. CoRR (2024)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version). CoRR (2023)
Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
Kater: Automating Weak Memory Model Metatheory and Consistency Checking. Proc. ACM Program. Lang. 7 (POPL) (2023)
Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav
Putting Weak Memory in Order via a Promising Intermediate Representation. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Abhishek Kr Singh, Ori Lahav
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency. Proc. ACM Program. Lang. 7 (POPL) (2023)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rely-Guarantee Reasoning for Causally Consistent Shared Memory. CAV (1) (2023)
Yotam Dvir, Ohad Kammar, Ori Lahav
An Algebraic Theory for Shared-State Concurrency. APLAS (2022)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
View-Based Owicki-Gries Reasoning for Persistent x86-TSO. ESOP (2022)
Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
Sequential reasoning for optimizing compilers under weak memory concurrency. PLDI (2022)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). CoRR (2022)
Ori Lahav, Yoni Zohar
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. IJCAR (2022)
Artem Khyzha, Ori Lahav
Abstraction for Crash-Resilient Objects. ESOP (2022)
Ori Lahav, Udi Boker
What's Decidable About Causally Consistent Shared Memory? ACM Trans. Program. Lang. Syst. 44 (2) (2022)
Artem Khyzha, Ori Lahav
Abstraction for Crash-Resilient Objects (Extended Version). CoRR (2021)
Ori Lahav, Guy Katz
Pruning and Slicing Neural Networks using Formal Verification. CoRR (2021)
Roy Margalit, Ori Lahav
Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang. 5 (POPL) (2021)
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
Making weak memory models fair. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Hans-J. Boehm, Ori Lahav, Azalea Raad
Foundations of Persistent Programming (Dagstuhl Seminar 21462). Dagstuhl Reports 11 (10) (2021)
Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav
Modular data-race-freedom guarantees in the promising semantics. PLDI (2021)
Ori Lahav, Guy Katz
Pruning and Slicing Neural Networks using Formal Verification. FMCAD (2021)
Artem Khyzha, Ori Lahav
Taming x86-TSO persistency. Proc. ACM Program. Lang. 5 (POPL) (2021)
Ori Lahav, Udi Boker
Decidable verification under a causally consistent shared memory. PLDI (2020)
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Reconciling Event Structures with Modern Multiprocessors. ECOOP (2020)
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Ser. 6 (2) (2020)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Artem Khyzha, Ori Lahav
Taming x86-TSO Persistency (Extended Version). CoRR (2020)
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
Making Weak Memory Models Fair. CoRR (2020)
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
Promising 2.0: global optimizations in relaxed memory concurrency. PLDI (2020)
Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, Viktor Vafeiadis
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3 (POPL) (2019)
Ori Lahav
Verification under causally consistent shared memory. ACM SIGLOG News 6 (2) (2019)
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis
Reconciling Event Structures with Modern Multiprocessors. CoRR (2019)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
On the Semantics of Snapshot Isolation. VMCAI (2019)
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3 (POPL) (2019)
Ori Lahav, João Marcos, Yoni Zohar
Correction to: Sequent Systems for Negative Modalities. Logica Universalis 13 (1) (2019)
Ori Lahav, Roy Margalit
Robustness against release/acquire semantics. PLDI (2019)
Ori Lahav, Yoni Zohar
Pure Sequent Calculi: Analyticity and Decision Procedure. ACM Trans. Comput. Log. 20 (3) (2019)
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
A Separation Logic for a Promising Semantics. ESOP (2018)
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2 (POPL) (2018)
Ori Lahav, Yoni Zohar
From the subformula property to cut-admissibility in propositional sequent calculi. J. Log. Comput. 28 (6) (2018)
Arnon Avron, Ori Lahav
A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5. Advances in Modal Logic (2018)
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. CoRR (2018)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
On the Semantics of Snapshot Isolation. CoRR (2018)
Azalea Raad, Ori Lahav, Viktor Vafeiadis
On Parallel Snapshot Isolation and Release/Acquire Consistency. ESOP (2018)
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
A promising semantics for relaxed-memory concurrency. POPL (2017)
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
Verifying Reachability in Networks with Mutable Datapaths. NSDI (2017)
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
Promising Compilation to ARMv8 POP. ECOOP (2017)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). Dagstuhl Artifacts Ser. 3 (2) (2017)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. ECOOP (2017)
Ori Lahav, João Marcos, Yoni Zohar
Sequent Systems for Negative Modalities. Logica Universalis 11 (3) (2017)
Ori Lahav, João Marcos, Yoni Zohar
Sequent systems for negative modalities. CoRR (2017)
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
Repairing sequential consistency in C/C++11. PLDI (2017)
Ori Lahav, Yoni Zohar
Cut-Admissibility as a Corollary of the Subformula Property. TABLEAUX (2017)
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
Verifying Reachability in Networks with Mutable Datapaths. CoRR (2016)
Ori Lahav, João Marcos, Yoni Zohar
It ain't necessarily so: Basic sequent systems for negative modalities. Advances in Modal Logic (2016)
Ori Lahav, João Marcos, Yoni Zohar
It ain't necessarily so: Basic sequent systems for negative modalities. CoRR (2016)
Ori Lahav
Semantic investigation of canonical Gödel hypersequent systems. J. Log. Comput. 26 (1) (2016)
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
Taming release-acquire consistency. POPL (2016)
Ori Lahav, Viktor Vafeiadis
Explaining Relaxed Memory Models with Program Transformations. FM (2016)
Ori Lahav, Viktor Vafeiadis
Owicki-Gries Reasoning for Weak Memory Models. ICALP (2) (2015)
Ori Lahav, Arnon Avron
A cut-free calculus for second-order Gödel logic. Fuzzy Sets Syst. 276 (2015)
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
Decentralizing SDN Policies. POPL (2015)
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. ACM Trans. Comput. Log. 16 (1) (2014)
Ori Lahav, Yoni Zohar
On the Construction of Analytic Sequent Calculi for Sub-classical Logics. WoLLIC (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
Modular reasoning about heap paths via effectively propositional formulas. POPL (2014)
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
Verifying Isolation Properties in the Presence of Middleboxes. CoRR (2014)
Carlos Cotrini, Yuri Gurevich, Ori Lahav, Artem Melentyev
Primal Infon Logic with Conjunctions as Sets. IFIP TCS (2014)
Ori Lahav, Yoni Zohar
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. IJCAR (2014)
Matthias Baaz, Ori Lahav, Anna Zamansky
Finite-valued Semantics for Canonical Labelled Calculi. J. Autom. Reason. 51 (4) (2013)
Ori Lahav, Arnon Avron
A unified semantic framework for fully structural propositional sequent systems. ACM Trans. Comput. Log. 14 (4) (2013)
Ori Lahav
Non-deterministic Multiple-Valued Matrices. J. Multiple Valued Log. Soft Comput. 21 (5-6) (2013)
Ori Lahav, Arnon Avron
A semantic proof of strong cut-admissibility for first-order Gödel logic. J. Log. Comput. 23 (1) (2013)
Ori Lahav
From Frame Properties to Hypersequent Rules in Modal Logics. LICS (2013)
Nikolaj Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) (2013)
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
Automated Support for the Investigation of Paraconsistent and Other Logics. LFCS (2013)
Matthias Baaz, Ori Lahav, Anna Zamansky
Effective Finite-Valued Semantics for Labelled Calculi. IJCAR (2012)
Ori Lahav
Non-deterministic Matrices for Semi-canonical Deduction Systems. ISMVL (2012)
Arnon Avron, Ori Lahav
A Multiple-Conclusion Calculus for First-Order Gödel Logic. CSR (2011)
Agata Ciabattoni, Ori Lahav, Anna Zamansky
Basic Constructive Connectives, Determinism and Matrix-Based Semantics. TABLEAUX (2011)
Arnon Avron, Ori Lahav
Kripke Semantics for Basic Sequent Systems. TABLEAUX (2011)
Ori Lahav, Arnon Avron
Non-deterministic Connectives in Propositional Godel Logic. EUSFLAT Conf. (2011)
Arnon Avron, Ori Lahav
Strict Canonical Constructive Systems. Fields of Logic and Computation (2010)
Arnon Avron, Ori Lahav
On Constructive Connectives and Systems Log. Methods Comput. Sci. 6 (4) (2010)
Arnon Avron, Ori Lahav
Canonical Constructive Systems. TABLEAUX (2009)