Interactive and automated proofs for graph transformations

DOI10.1017/S096012951800021XzbMath1398.68286WikidataQ113857440 ScholiaQ113857440MaRDI QIDQ4585009

Martin Strecker

Publication date: 5 September 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Theorem proving graph grammars with attributes and negative application conditions, Unnamed Item, Unnamed Item, Monadic second-order incorrectness logic for GP 2

Uses Software

• Isabelle/HOL
• VIATRA2
• GROOVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verification of graph grammars using a logical approach
• A framework for the verification of infinite-state graph transformation systems
• Reasoning with graph constraints
• Isabelle/HOL. A proof assistant for higher-order logic
• The model transformation language of the VIATRA2 framework
• A logic of reachable patterns in linked data-structures
• Hoare-Style Verification of Graph Programs
• Resolution-Like Theorem Proving for High-Level Conditions
• Weakest Preconditions for High-Level Programs
• Correctness of high-level transformation systems relative to nested conditions
• A Dynamic Logic for Termgraph Rewriting
• Formal Verification of Graph Grammars using Mathematical Induction
• Computer Science Logic
• Computer Aided Verification