Cover Image

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Grandury, Marcos, Nanevski, Aleksandar, Gryzlov, Alexander
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

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

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

JAX Autodiff from a Linear Logic Perspective (Extended Version)
by: Giusti, Giulia, et al.
Published: (2025)

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

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

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

Adjoint Natural Deduction (Extended Version)
by: Jang, Junyoung, et al.
Published: (2024)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

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

Hybrid Intersection Types for PCF (Extended Version)
by: Barenbaum, Pablo, et al.
Published: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
by: Pincus, Jared, et al.
Published: (2024)

Monadic Intersection Types, Relationally (Extended Version)
by: Gavazzo, Francesco, et al.
Published: (2024)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, 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)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
by: Lööw, Andreas, et al.
Published: (2024)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
by: Gladshtein, Vladimir, et al.
Published: (2024)

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)

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

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
by: Lahav, Ori, et al.
Published: (2023)

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)

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

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

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
by: Voichick, Finn, et al.
Published: (2022)

A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)
by: Ambal, Guillaume, et al.
Published: (2025)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Verifying Floating-Point Programs in Stainless
by: Gilot, Andrea, et al.
Published: (2026)

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

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
by: Deng, Haotian, et al.
Published: (2025)

GATlab: Modeling and Programming with Generalized Algebraic Theories
by: Lynch, Owen, et al.
Published: (2024)

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

Verifying Solutions to Semantics-Guided Synthesis Problems
by: Murphy, Charlie, et al.
Published: (2024)

Verifying Peephole Rewriting In SSA Compiler IRs
by: Bhat, Siddharth, et al.
Published: (2024)

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

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

To bind or not to bind? Discovering Stable Relationships in Object-centric Processes (Extended Version)
by: Seidel, Anjo, et al.
Published: (2025)