A decidable fragment in separation logic with inductive predicates and arithmetic
From MaRDI portal
Publication:2164251
DOI10.1007/978-3-319-63390-9_26zbMath1497.03048OpenAlexW2613252377MaRDI QIDQ2164251
Quang Loc Le, Wei-Ngan Chin, Jun Sun, Makoto Tatsuta
Publication date: 12 August 2022
Full work available at URL: https://ink.library.smu.edu.sg/sis_research/4702
Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
An efficient cyclic entailment procedure in a fragment of separation logic, Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation, Strong-separation logic, Compositional satisfiability solving in separation logic, Unnamed Item, Reasoning about block-based cloud storage systems via separation logic, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions