Inductive invariant checking with partial negative application conditions

DOI10.1007/978-3-319-21145-9_15MaRDI QIDQ2947222zbMATH OpenOpenAlexFDO

Authors Johannes Dyck, Holger Giese

Publication date 22 September 2015

Published in Graph Transformation (Search for Journal in Brave)

Full work available at URL https://nbn-resolving.org/urn:nbn:de:kobv:517-opus4-77748

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• \(k\)-inductive invariant checking for graph transformation systems
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Efficient symbolic implementation of graph automata with applications to invariant checking
• Towards automated software model checking using graph transformation systems and bogor
• 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 general framework for well-structured graph transformation systems
• Correctness of high-level transformation systems relative to nested conditions
• Efficient symbolic implementation of graph automata with applications to invariant checking
• Fundamentals of algebraic graph transformation
• scientific article; zbMATH DE number 1863175 (Why is no real title available?)
• Inductive invariant checking with partial negative application conditions
• Towards automatic verification of behavior preservation for model transformation via invariant checking

Cited in

(10)

• Towards automated software model checking using graph transformation systems and bogor
• A tale of two graph models: a case study in wireless sensor networks
• Efficient symbolic implementation of graph automata with applications to invariant checking
• Inductive invariant checking with partial negative application conditions
• Application of Graph Transformation in Verification of Dynamic Systems
• scientific article; zbMATH DE number 2016085 (Why is no real title available?)
• \(k\)-inductive invariant checking for graph transformation systems
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
• Constructing optimized constraint-preserving application conditions for model transformation rules

This page was built for publication: Inductive invariant checking with partial negative application conditions

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