Deciding Entailments in Inductive Separation Logic with Tree Automata
From MaRDI portal
Publication:3457790
DOI10.1007/978-3-319-11936-6_15zbMath1448.68266arXiv1402.2127OpenAlexW1757770995MaRDI QIDQ3457790
Tomáš Vojnar, Adam Rogalewicz, Radu Iosif
Publication date: 17 December 2015
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1402.2127
Formal languages and automata (68Q45) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items
Program Verification with Separation Logic, Decision Procedure for Entailment of Symbolic Heaps with Arrays, Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic, Logic programming approach to automata-based decision procedures, Automated mutual induction proof in separation logic, Unnamed Item, A proof procedure for separation logic with inductive definitions and data, Compositional entailment checking for a fragment of separation logic, An efficient cyclic entailment procedure in a fragment of separation logic, An undecidability result for separation logic with theory reasoning, Foundations for entailment checking in quantitative separation logic, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Strong-separation logic, Compositional satisfiability solving in separation logic, Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps, Unnamed Item, A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, Unifying decidable entailments in separation logic with inductive definitions, Slide, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
