Decidable logics combining heap structures and data
DOI10.1145/1926385.1926455zbMATH Open1284.68411OpenAlexW4238367836MaRDI QIDQ5408581FDOQ5408581
Xiaokang Qiu, Parthasarathy 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) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cited In (17)
- Compositional satisfiability solving in separation logic
- Heaps and Data Structures: A Challenge for Automated Provers
- Reachability of scope-bounded multistack pushdown systems
- Nested antichains for WS1S
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Separation logics and modalities: a survey
- Lazy Automata Techniques for WS1S
- A shape graph logic and a shape system
- Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
- Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
- Juggrnaut: using graph grammars for abstracting unbounded heap structures
- Reasoning About Data Trees Using CHCs
- Parametrized invariance for infinite state processes
- Forest automata for verification of heap manipulation
- Reasoning about algebraic data types with abstractions
- Strong-separation logic
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
Uses Software
This page was built for publication: Decidable logics combining heap structures and data
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408581)
