The Tree Width of Separation Logic with Recursive Definitions
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F13%3APU106318" target="_blank" >RIV/00216305:26230/13:PU106318 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/chapter/10.1007/978-3-642-38574-2_2" target="_blank" >http://link.springer.com/chapter/10.1007/978-3-642-38574-2_2</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-38574-2_2" target="_blank" >10.1007/978-3-642-38574-2_2</a>
Alternative languages
Result language
angličtina
Original language name
The Tree Width of Separation Logic with Recursive Definitions
Original language description
Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general decidability result. We prove that any Separation Logic formula using rather general recursively defined predicates is decidable for satisfiability, and moreover, entailments between such formulae are decidable for validity. These predicates are general enough to define (doubly-) linked lists, trees, and structures more general than trees, such as trees whose leaves are chained in a list. The decidability proofs are by reduction to decidability ofMonadic Second Order Logic on graphs with bounded tree width.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Automated Deduction - CADE-24
ISBN
978-3-642-38573-5
ISSN
0302-9743
e-ISSN
—
Number of pages
18
Pages from-to
21-38
Publisher name
Springer Verlag
Place of publication
Berlin
Event location
The Crowne Plaza Resort in Lake Placid, New York
Event date
Jun 9, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—