Juggrnaut: using graph grammars for abstracting unbounded heap structures
DOI10.1007/s10703-015-0236-1zbMath1341.68033OpenAlexW2110895665WikidataQ57800682 ScholiaQ57800682MaRDI QIDQ746781
Christina Jansen, Joost-Pieter Katoen, Jonathan Heinen, Thomas Noll
Publication date: 20 October 2015
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-015-0236-1
software verificationdynamic data structuresheap abstractionhyperedge replacement grammarspointer-manipulating programs
Grammars and rewriting systems (68Q42) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- S-functions for graphs
- Proving pointer programs in higher-order logic
- The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
- Hoare-Style Verification of Graph Programs
- A Local Greibach Normal Form for Hyperedge Replacement Grammars
- Generating Abstract Graph-Based Procedure Summaries for Pointer Programs
- Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs
- Separation and information hiding
- Scalable Shape Analysis for Systems Code
- Abstracting Complex Data Structures by Hyperedge Replacement
- Safety and Liveness in Concurrent Pointer Programs
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
- The Tree Width of Separation Logic with Recursive Definitions
- A Greibach normal form for context-free graph grammars
- Programming Languages and Systems
- Decidable logics combining heap structures and data
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- An efficient machine-independent procedure for garbage collection in various list structures
- Programs with Lists Are Counter Automata
This page was built for publication: Juggrnaut: using graph grammars for abstracting unbounded heap structures
