Generating inductive predicates for symbolic execution of pointer-manipulating programs

DOI10.1007/978-3-319-09108-2_5MaRDI QIDQ3192224zbMATH OpenOpenAlexFDO

Authors Christina Jansen, Florian Göbe, Thomas Noll

Publication date 26 September 2014

Published in Graph Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-09108-2_5

Mathematics Subject Classification ID

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

Recommendations

• Generating abstract graph-based procedure summaries for pointer programs
• Verification, Model Checking, and Abstract Interpretation
• Tree-like grammars and separation logic
• Programming Languages and Systems
• On automated lemma generation for separation logic with inductive definitions

Cited in

(4)

• Generating abstract graph-based procedure summaries for pointer programs
• Abstracting Complex Data Structures by Hyperedge Replacement
• A proof procedure for separation logic with inductive definitions and data
• Juggrnaut: using graph grammars for abstracting unbounded heap structures

This page was built for publication: Generating inductive predicates for symbolic execution of pointer-manipulating programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192224)