Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic

DOI10.1007/978-3-319-47958-3_22zbMath1485.03078OpenAlexW2528592500MaRDI QIDQ3179308

Makoto Tatsuta, Wei-Ngan Chin, Quang Loc Le

Publication date: 21 December 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://research.tees.ac.uk/ws/files/7855974/621147.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) First-order arithmetic and fragments (03F30)

Related Items (3)

Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation ⋮ Compositional satisfiability solving in separation logic ⋮ Unnamed Item

Uses Software

• Slide

Cites Work

• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Quantitative separation logic and programs with lists
• Model checking for symbolic-heap separation logic with inductive predicates
• Separation Logic Modulo Theories
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• A decision procedure for satisfiability in separation logic with inductive predicates
• The Tree Width of Separation Logic with Recursive Definitions
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems

This page was built for publication: Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic