Modeling and verifying graph transformations in proof assistants
From MaRDI portal
Publication:2870320
DOI10.1016/J.ENTCS.2008.03.039zbMATH Open1279.68297OpenAlexW2159151953MaRDI QIDQ2870320FDOQ2870320
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
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
Graph theory (including graph drawing) in computer science (68R10) Grammars and rewriting systems (68Q42)
Cites Work
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Foundations of Software Science and Computation Structures
- Explicit State Model Checking for Graph Grammars
- Logic for Programming, Artificial Intelligence, and Reasoning
- Abstract graph transformation
- Title not available (Why is that?)
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
- Towards common exchange formats for graphs and graph transformation systems
Cited In (14)
- Theorem proving graph grammars: strategies for discharging proof obligations
- Resolution-Like Theorem Proving for High-Level Conditions
- Specification and verification of graph-based model transformation properties
- Verification of graph grammars using a logical approach
- Theorem proving graph grammars with attributes and negative application conditions
- A type-theoretic framework for certified model transformations
- Interactive and automated proofs for graph transformations
- Verifying a behavioural logic for graph transformation systems
- Verifying graph transformation systems with description logics
- 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
- Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations
- Ensuring correctness of model transformations while remaining decidable
Uses Software
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)
