Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions

DOI10.1007/978-3-030-51372-6_15MaRDI QIDQ5100737zbMATHOpenAlexFDO

Authors Sven Schneider, Johannes Dyck, Holger Giese

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

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

Recommendations

• \(k\)-inductive invariant checking for graph transformation systems
• Towards the Verification of Attributed Graph Transformation Systems
• Inductive invariant checking with partial negative application conditions
• Theorem proving graph grammars with attributes and negative application conditions
• Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction

Cites work

• -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation
• A Modal-Logic Based Graph Abstraction
• Attributed Graph Constraints
• Correctness of high-level transformation systems relative to nested conditions
• Delaying Constraint Solving in Symbolic Graph Transformation
• Fundamentals of algebraic graph transformation
• GitHub
• Inductive invariant checking with partial negative application conditions
• Lazy graph transformation
• Probabilistic timed graph transformation systems
• Programming Languages and Systems
• Rewriting abstract structures: materialization explained categorically
• Sound and complete abstract graph transformation
• Symbolic graphs for attributed graph constraints
• Verifying monadic second-order properties of graph programs
• \(k\)-inductive invariant checking for graph transformation systems

Cited in

(18)

• Monadic second-order incorrectness logic for GP 2
• Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic
• Inductive invariant checking with partial negative application conditions
• Compositional analysis of probabilistic timed graph transformation systems
• Compositional analysis of probabilistic timed graph transformation systems
• Incorrectness logic for graph programs
• Efficient symbolic implementation of graph automata with applications to invariant checking
• Analysis of graph transformation systems: native vs translation-based techniques
• Application of Graph Transformation in Verification of Dynamic Systems
• Optimistic and pessimistic on-the-fly analysis for metric temporal graph logic
• Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
• \(k\)-inductive invariant checking for graph transformation systems
• scientific article; zbMATH DE number 2016085 (Why is no real title available?)
• Theorem proving graph grammars with attributes and negative application conditions
• A framework for the verification of infinite-state graph transformation systems
• On the Use of Alloy to Analyze Graph Transformation Systems
• Towards the Verification of Attributed Graph Transformation Systems
• Checking bisimilarity for attributed graph transformation

Describes a project that uses

Uses Software

• GitHub

This page was built for publication: Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions

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