Ori Lahav

Proceedings of the Programming Languages and Systems, 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2022

Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

An Algebraic Theory for Shared-State Concurrency.

[BibT_eX]

[DOI]

Yotam Dvir

Ohad Kammar

Proceedings of the Programming Languages and Systems - 20th Asian Symposium, 2022

2021

Verifying observational robustness against a c11-style memory model.

[BibT_eX]

[DOI]

Roy Margalit

Proc. ACM Program. Lang., 2021

Making weak memory models fair.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Taming x86-TSO persistency.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Foundations of Persistent Programming (Dagstuhl Seminar 21462).

[BibT_eX]

[DOI]

Hans-Juergen Boehm

Dagstuhl Reports, 2021

Abstraction for Crash-Resilient Objects (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2021

Modular data-race-freedom guarantees in the promising semantics.

[BibT_eX]

[DOI]

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Reconciling Event Structures with Modern Multiprocessors (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2020

Taming x86-TSO Persistency (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2020

Promising 2.0: global optimizations in relaxed memory concurrency.

[BibT_eX]

[DOI]

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Decidable verification under a causally consistent shared memory.

[BibT_eX]

[DOI]

Udi Boker

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Reconciling Event Structures with Modern Multiprocessors.

[BibT_eX]

[DOI]

Proceedings of the 34th European Conference on Object-Oriented Programming, 2020

2019

Pure Sequent Calculi: Analyticity and Decision Procedure.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2019

Verification under causally consistent shared memory.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2019

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Bridging the gap between programming languages and hardware weak memory models.

[BibT_eX]

[DOI]

Anton Podkopaev

Proc. ACM Program. Lang., 2019

Correction to: Sequent Systems for Negative Modalities.

[BibT_eX]

[DOI]

João Marcos

Logica Universalis, 2019

On the Semantics of Snapshot Isolation.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

Robustness against release/acquire semantics.

[BibT_eX]

[DOI]

Roy Margalit

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018

Effective stateless model checking for C/C++ concurrency.

[BibT_eX]

[DOI]

Michalis Kokologiannakis

Konstantinos Sagonas

Proc. ACM Program. Lang., 2018

From the subformula property to cut-admissibility in propositional sequent calculi.

[BibT_eX]

[DOI]

J. Log. Comput., 2018

A Separation Logic for a Promising Semantics.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

On Parallel Snapshot Isolation and Release/Acquire Consistency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

A Simple Cut-Free System for a Paraconsistent Logic Equivalent to S5.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 12, 2018

2017

Sequent Systems for Negative Modalities.

[BibT_eX]

[DOI]

João Marcos

Logica Universalis, 2017

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2017

Cut-Admissibility as a Corollary of the Subformula Property.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2017

A promising semantics for relaxed-memory concurrency.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Repairing sequential consistency in C/C++11.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Verifying Reachability in Networks with Mutable Datapaths.

[BibT_eX]

[DOI]

Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, 2017

Promising Compilation to ARMv8 POP.

[BibT_eX]

[DOI]

Anton Podkopaev

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.

[BibT_eX]

[DOI]

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016

Semantic investigation of canonical Gödel hypersequent systems.

[BibT_eX]

[DOI]

J. Log. Comput., 2016

Taming release-acquire consistency.

[BibT_eX]

[DOI]

Nick Giannarakis

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Explaining Relaxed Memory Models with Program Transformations.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

It ain't necessarily so: Basic sequent systems for negative modalities.

[BibT_eX]

[DOI]

João Marcos

Proceedings of the Advances in Modal Logic 11, 2016

2015

A cut-free calculus for second-order Gödel logic.

[BibT_eX]

[DOI]

Fuzzy Sets Syst., 2015

Decentralizing SDN Policies.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Owicki-Gries Reasoning for Weak Memory Models.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

2014

Semantic investigation of proof systems for non-classical logics

[BibT_eX]

[DOI]

PhD thesis, 2014

Taming Paraconsistent (and Other) Logics: An Algorithmic Approach.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2014

Verifying Isolation Properties in the Presence of Middleboxes.

[BibT_eX]

[DOI]

CoRR, 2014

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

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, Information, and Computation, 2014

Modular reasoning about heap paths via effectively propositional formulas.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Primal Infon Logic with Conjunctions as Sets.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2014

SAT-Based Decision Procedure for Analytic Pure Sequent Calculi.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

A unified semantic framework for fully structural propositional sequent systems.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2013

Studying Sequent Systems <i>via</i> Non-deterministic Multiple-Valued Matrices.

[BibT_eX]

[DOI]

J. Multiple Valued Log. Soft Comput., 2013

A semantic proof of strong cut-admissibility for first-order Gödel logic.

[BibT_eX]

[DOI]

J. Log. Comput., 2013

Finite-valued Semantics for Canonical Labelled Calculi.

[BibT_eX]

[DOI]

Matthias Baaz

Anna Zamansky

J. Autom. Reason., 2013

Instantiations, Zippers and EPR Interpolation.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

From Frame Properties to Hypersequent Rules in Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Automated Support for the Investigation of Paraconsistent and Other Logics.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2013

2012

Non-deterministic Matrices for Semi-canonical Deduction Systems.

[BibT_eX]

[DOI]

Proceedings of the 42nd IEEE International Symposium on Multiple-Valued Logic, 2012

Effective Finite-Valued Semantics for Labelled Calculi.

[BibT_eX]

[DOI]

Matthias Baaz

Anna Zamansky

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Basic Constructive Connectives, Determinism and Matrix-Based Semantics.

[BibT_eX]

[DOI]

Agata Ciabattoni

Anna Zamansky

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

Kripke Semantics for Basic Sequent Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

Non-deterministic Connectives in Propositional Godel Logic.

[BibT_eX]

[DOI]

Proceedings of the 7th conference of the European Society for Fuzzy Logic and Technology, 2011

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

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2011

2010

On Constructive Connectives and Systems

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2010

Strict Canonical Constructive Systems.

[BibT_eX]

[DOI]

Proceedings of the Fields of Logic and Computation, 2010

2009

Canonical Constructive Systems.

[BibT_eX]

[DOI]