An undecidability result for separation logic with theory reasoning

DOI10.1016/j.ipl.2023.106359OpenAlexW4315478779MaRDI QIDQ6161426

Mnacho Echenim, Nicolas Peltier

Publication date: 5 June 2023

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2023.106359

zbMATH Keywords

decidabilityseparation logicautomatic theorem provinginductive definition

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Satisfiability of compositional separation logic with tree predicates and data constraints
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• The Tree Width of Separation Logic with Recursive Definitions
• BI as an assertion language for mutable data structures

This page was built for publication: An undecidability result for separation logic with theory reasoning