Modeling and verifying graph transformations in proof assistants

DOI10.1016/J.ENTCS.2008.03.039MaRDI QIDQ2870320zbMATH OpenOpenAlexFDO

Authors Martin Strecker

Publication date 17 January 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.03.039

zbMATH Keywords

graph transformationstheorem proving

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• Interactive and automated proofs for graph transformations
• Ensuring correctness of model transformations while remaining decidable
• Verifying graph transformation systems with description logics
• Sound and complete abstract graph transformation
• Specification and verification of graph-based model transformation properties

Cites work

• Abstract graph transformation
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Explicit State Model Checking for Graph Grammars
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 177461 (Why is no real title available?)
• scientific article; zbMATH DE number 1142315 (Why is no real title available?)
• scientific article; zbMATH DE number 969070 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Towards common exchange formats for graphs and graph transformation systems

Cited in

(14)

• Verifying graph transformation systems with description logics
• Theorem proving graph grammars with attributes and negative application conditions
• Verifying a behavioural logic for graph transformation systems
• A type-theoretic framework for certified model transformations
• Ensuring correctness of model transformations while remaining decidable
• Specification and verification of graph-based model transformation properties
• Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations
• Resolution-Like Theorem Proving for High-Level Conditions
• Verification of graph grammars using a logical approach
• Interactive and automated proofs for graph transformations
• Theorem proving graph grammars: strategies for discharging proof obligations
• Formal verification of graph grammars using mathematical induction
• Towards mechanised proofs in double-pushout graph transformation
• Specification and verification of a linear-time temporal logic for graph transformation

Describes a project that uses

Uses Software

• Isabelle/HOL
• AGG

This page was built for publication: Modeling and verifying graph transformations in proof assistants

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