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
Recommendations
- A logic of reachable patterns in linked data-structures
- scientific article; zbMATH DE number 1841809
- Foundations of Software Science and Computation Structures
- A Logic-Based Framework for Reasoning about Composite Data Structures
- Modular reasoning about heap paths via effectively propositional formulas
Formal languages and automata (68Q45) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cited In (19)
- 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
- A logic of reachable patterns in linked data-structures
- A Logic-Based Framework for Reasoning about Composite Data Structures
- 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)
