Cover Image

Context-Aware Separation Logic

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Meyer, Roland, Wies, Thomas, Wolff, Sebastian
Format:	Preprint
Published:	2023
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Arithmetizing Shape Analysis
by: Wolff, Sebastian, et al.
Published: (2024)

Realizability in Semantics-Guided Synthesis Done Eagerly
by: Meyer, Roland, et al.
Published: (2024)

Implementability of Global Distributed Protocols modulo Network Architectures
by: Li, Elaine, et al.
Published: (2026)

Consistent Updates for Scalable Microservices
by: Chait-Roth, Devora, et al.
Published: (2025)

Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
by: Nicola, Mihai, et al.
Published: (2024)

Verifying Lock-free Search Structure Templates
by: Patel, Nisarg, et al.
Published: (2024)

Characterizing Implementability of Global Protocols with Infinite States and Data
by: Li, Elaine, et al.
Published: (2024)

Hyper Separation Logic (extended version)
by: Gospodinov, Trayan, et al.
Published: (2026)

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

Verification Algorithms for Automated Separation Logic Verifiers
by: Eilers, Marco, et al.
Published: (2024)

Complete Multiparty Session Type Projection with Automata
by: Li, Elaine, et al.
Published: (2023)

MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
by: Leißa, Roland, et al.
Published: (2024)

Tail Modulo Cons, OCaml, and Relational Separation Logic
by: Allain, Clément, et al.
Published: (2024)

Oriented Metrics for Bottom-Up Enumerative Synthesis
by: Meyer, Roland, et al.
Published: (2025)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
by: Dardinier, Thibault, et al.
Published: (2024)

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

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
by: Ling, Hongyi, et al.
Published: (2026)

Agentic Separation Logic Specification Synthesis
by: Suresh, Tarun, et al.
Published: (2026)

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

Stellis: A Strategy Language for Purifying Separation Logic Entailments
by: Wang, Zhiyi, et al.
Published: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

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)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
by: Ramananandro, Tahina, et al.
Published: (2025)

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

QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei, et al.
Published: (2025)

Bayesian Separation Logic
by: Ho, Shing Hin, et al.
Published: (2025)

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

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

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
by: van der Wall, Sören, et al.
Published: (2024)

From Program Logics to Language Logics
by: Cimini, Matteo
Published: (2024)

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

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

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

Cerisier: A Program Logic for Attestation in a Capability Machine
by: Rousseau, June, et al.
Published: (2026)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
by: Nagy, Shaan, et al.
Published: (2024)

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

Separating Sessions Smoothly
by: Fowler, Simon, et al.
Published: (2021)

Causality and Semantic Separation
by: Zhang, Anna, et al.
Published: (2026)