Juggrnaut: using graph grammars for abstracting unbounded heap structures

DOI10.1007/S10703-015-0236-1zbMath1341.68033DBLPjournals/fmsd/HeinenJKN15OpenAlexW2110895665WikidataQ57800682 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

zbMATH Keywords

software verificationdynamic data structuresheap abstractionhyperedge replacement grammarspointer-manipulating programs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Juggrnaut

Uses Software

• MONA
• Smallfoot
• Slide

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