Decidable logics combining heap structures and data
From MaRDI portal
Publication:5408581
DOI10.1145/1926385.1926455zbMath1284.68411OpenAlexW4238367836MaRDI QIDQ5408581
Xiaokang Qiu, P. Madhusudan, Gennaro Parlato
Publication date: 10 April 2014
Published in: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://eprints.soton.ac.uk/272448/1/popl-strand.pdf
Formal languages and automata (68Q45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)
Related Items (15)
Separation logics and modalities: a survey ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Reasoning about algebraic data types with abstractions ⋮ Forest automata for verification of heap manipulation ⋮ Reachability of scope-bounded multistack pushdown systems ⋮ Nested antichains for WS1S ⋮ Strong-separation logic ⋮ Parametrized invariance for infinite state processes ⋮ Compositional satisfiability solving in separation logic ⋮ Lazy Automata Techniques for WS1S ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ A shape graph logic and a shape system ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Juggrnaut: using graph grammars for abstracting unbounded heap structures
Uses Software
This page was built for publication: Decidable logics combining heap structures and data