Modeling and Verifying Graph Transformations in Proof Assistants

DOI10.1016/j.entcs.2008.03.039zbMath1279.68297OpenAlexW2159151953MaRDI QIDQ2870320

Martin Strecker

Publication date: 17 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.03.039

zbMATH Keywords

theorem provinggraph transformations

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Grammars and rewriting systems (68Q42)

Related Items

Theorem proving graph grammars with attributes and negative application conditions ⋮ Verification of graph grammars using a logical approach ⋮ Resolution-Like Theorem Proving for High-Level Conditions ⋮ Formal Verification of Graph Grammars using Mathematical Induction

Uses Software

• Isabelle/HOL
• AGG

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Explicit State Model Checking for Graph Grammars
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Towards Common Exchange Formats for Graphs and Graph Transformation Systems
• Logic for Programming, Artificial Intelligence, and Reasoning
• Foundations of Software Science and Computation Structures