Cover Image

Compositional Verification in Concurrent Separation Logic with Permissions Regions

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Le, Quang Loc
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Towards Concurrent Quantitative Separation Logic
by: Fesefeldt, Ira, et al.
Published: (2022)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
by: Zilberstein, Noam, et al.
Published: (2024)

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
by: Zimmerman, Conrad, et al.
Published: (2024)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

FO-Complete Program Verification for Heap Logics
by: Murali, Adithya, et al.
Published: (2026)

A Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
by: Zilberstein, Noam, et al.
Published: (2023)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

On the Expressivity of Typed Concurrent Calculi
by: Paulus, Joseph William Neal
Published: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

A Lazy, Concurrent Convertibility Checker
by: Courant, Nathanaëlle, et al.
Published: (2025)

Typed Non-determinism in Concurrent Calculi: The Eager Way
by: Heuvel, Bas van den, et al.
Published: (2024)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
by: Hansen, Zachary
Published: (2025)

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
by: Bollig, Benedikt
Published: (2026)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency
by: Derakhshan, Farzaneh, et al.
Published: (2024)

Unrealizability Logic
by: Kim, Jinwoo, et al.
Published: (2022)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications
by: Casetta, Richard, et al.
Published: (2026)

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
by: Sulzmann, Martin
Published: (2026)

Automated Software Verification of Hyperliveness
by: Beutner, Raven
Published: (2024)

Partial Incorrectness Logic
by: Verscht, Lena, et al.
Published: (2025)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
by: Zilberstein, Noam
Published: (2024)

Predictable Verification using Intrinsic Definitions
by: Murali, Adithya, et al.
Published: (2024)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Logic Programming with Extensible Types
by: Perez, Ivan, et al.
Published: (2026)

Finite-Choice Logic Programming
by: Martens, Chris, et al.
Published: (2024)

Compositional Program Verification with Polynomial Functors in Dependent Type Theory
by: Aberlé, C. B.
Published: (2026)

Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
by: Nemati, Hamed, et al.
Published: (2025)

Ordered Adjoint Logic (Extended Version)
by: Roshal, Sophia, et al.
Published: (2026)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, et al.
Published: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
by: Sotoudeh, Matthew
Published: (2025)