Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
DOI10.1007/978-3-030-51372-6_15zbMATH Open1502.68160OpenAlexW3037116850MaRDI QIDQ5100737FDOQ5100737
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
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
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- GitHub
- A Modal-Logic Based Graph Abstraction
- Verifying monadic second-order properties of graph programs
- Correctness of high-level transformation systems relative to nested conditions
- Fundamentals of algebraic graph transformation
- Attributed Graph Constraints
- Delaying Constraint Solving in Symbolic Graph Transformation
- Symbolic graphs for attributed graph constraints
- -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation
- Inductive invariant checking with partial negative application conditions
- \(k\)-inductive invariant checking for graph transformation systems
- Programming Languages and Systems
- Lazy graph transformation
- Probabilistic timed graph transformation systems
- Rewriting abstract structures: materialization explained categorically
- Sound and complete abstract graph transformation
Cited In (18)
- Checking bisimilarity for attributed graph transformation
- Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic
- Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
- Theorem proving graph grammars with attributes and negative application conditions
- A framework for the verification of infinite-state graph transformation systems
- Application of Graph Transformation in Verification of Dynamic Systems
- Optimistic and pessimistic on-the-fly analysis for metric temporal graph logic
- Compositional analysis of probabilistic timed graph transformation systems
- Compositional analysis of probabilistic timed graph transformation systems
- Analysis of graph transformation systems: native vs translation-based techniques
- Efficient symbolic implementation of graph automata with applications to invariant checking
- Title not available (Why is that?)
- Inductive invariant checking with partial negative application conditions
- \(k\)-inductive invariant checking for graph transformation systems
- On the Use of Alloy to Analyze Graph Transformation Systems
- Towards the Verification of Attributed Graph Transformation Systems
- Monadic second-order incorrectness logic for GP 2
- Incorrectness logic for graph programs
Uses Software
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)