Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions

DOI10.1007/978-3-030-51372-6_15zbMath1502.68160OpenAlexW3037116850MaRDI QIDQ5100737

Holger Giese, Sven Schneider, Johannes Dyck

Publication date: 1 September 2022

Published in: Graph Transformation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51372-6_15

zbMATH Keywords

Isabellesymbolic graphsk-inductionformal static analysissymbolic state space abstraction

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (5)

Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Compositional analysis of probabilistic timed graph transformation systems ⋮ Monadic second-order incorrectness logic for GP 2 ⋮ Incorrectness logic for graph programs

Uses Software

• GitHub

Cites Work

• GitHub
• Symbolic graphs for attributed graph constraints
• Probabilistic timed graph transformation systems
• Rewriting abstract structures: materialization explained categorically
• Fundamentals of algebraic graph transformation
• Lazy Graph Transformation
• Inductive Invariant Checking with Partial Negative Application Conditions
• Sound and Complete Abstract Graph Transformation
• Verifying Monadic Second-Order Properties of Graph Programs
• Attributed Graph Constraints
• A Modal-Logic Based Graph Abstraction
• Correctness of high-level transformation systems relative to nested conditions
• Delaying Constraint Solving in Symbolic Graph Transformation
• k-Inductive Invariant Checking for Graph Transformation Systems
• Programming Languages and Systems
• -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation

This page was built for publication: Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions