Buchumschlag

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Elad, Neta, Murali, Adithya, Shoham, Sharon
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Logic in Computer Science Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Axe 'Em: Eliminating Spurious States with Induction Axioms
von: Elad, Neta, et al.
Veröffentlicht: (2024)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
von: Elad, Neta, et al.
Veröffentlicht: (2023)

Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
von: Elad, Neta, et al.
Veröffentlicht: (2026)

FO-Complete Program Verification for Heap Logics
von: Murali, Adithya, et al.
Veröffentlicht: (2026)

Predictable Verification using Intrinsic Definitions
von: Murali, Adithya, et al.
Veröffentlicht: (2024)

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
von: Lotan, Raz, et al.
Veröffentlicht: (2026)

Complete first-order reasoning for functional programs
von: Murali, Adithya, et al.
Veröffentlicht: (2026)

Recursive Mutexes in Separation Logic
von: Du, Ke, et al.
Veröffentlicht: (2026)

Towards Concurrent Quantitative Separation Logic
von: Fesefeldt, Ira, et al.
Veröffentlicht: (2022)

A Nominal Approach to Probabilistic Separation Logic
von: Li, John M., et al.
Veröffentlicht: (2024)

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
von: Su, Wanyun, et al.
Veröffentlicht: (2024)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
von: Le, Quang Loc
Veröffentlicht: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
von: Mathiasen, Anders Alnor, et al.
Veröffentlicht: (2025)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
von: Haselwarter, Philipp G., et al.
Veröffentlicht: (2024)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
von: Zilberstein, Noam, et al.
Veröffentlicht: (2023)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
von: Timany, Amin, et al.
Veröffentlicht: (2021)

Implicit Rankings for Verifying Liveness Properties in First-Order Logic
von: Lotan, Raz, et al.
Veröffentlicht: (2024)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
von: Tsukada, Takeshi, et al.
Veröffentlicht: (2025)

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

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

The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
von: Bozga, Marius, et al.
Veröffentlicht: (2023)

Proving Cutoff Bounds for Safety Properties in First-Order Logic
von: Lotan, Raz, et al.
Veröffentlicht: (2024)

Cyclic Proofs in Hoare Logic and its Reverse
von: Brotherston, James, et al.
Veröffentlicht: (2025)

Bayesian Separation Logic
von: Ho, Shing Hin, et al.
Veröffentlicht: (2025)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
von: Vollmer, Victoria, et al.
Veröffentlicht: (2024)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
von: Frenkel, Eden, et al.
Veröffentlicht: (2026)

Structural Temporal Logic for Mechanized Program Verification
von: Ioannidis, Eleftherios, et al.
Veröffentlicht: (2024)

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
von: Bueri, Lucas, et al.
Veröffentlicht: (2024)

Relative Completeness of Incorrectness Separation Logic
von: Lee, Yeonseok, et al.
Veröffentlicht: (2025)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
von: Zimmerman, Conrad, et al.
Veröffentlicht: (2024)

Coinductive Proofs for Temporal Hyperliveness
von: Correnson, Arthur, et al.
Veröffentlicht: (2025)

Symmetric Proofs of Parameterized Programs
von: Cheng, Ruotong, et al.
Veröffentlicht: (2026)

Unrealizability Logic
von: Kim, Jinwoo, et al.
Veröffentlicht: (2022)

More Church-Rosser Proofs in BELUGA
von: Momigliano, Alberto, et al.
Veröffentlicht: (2024)

RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
von: Matsushita, Yusuke, et al.
Veröffentlicht: (2025)

Pleasant Imperative Program Proofs with GallinaC
von: Fort, Frédéric, et al.
Veröffentlicht: (2025)

Partial Incorrectness Logic
von: Verscht, Lena, et al.
Veröffentlicht: (2025)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
von: Zilberstein, Noam
Veröffentlicht: (2024)

Zippy -- Generic White-Box Proof Search with Zippers
von: Kappelmann, Kevin
Veröffentlicht: (2025)

Logic Programming with Extensible Types
von: Perez, Ivan, et al.
Veröffentlicht: (2026)