Verification of graph grammars using a logical approach

DOI10.1016/J.SCICO.2010.02.006MaRDI QIDQ436370zbMATH OpenOpenAlexFDO

Authors Simone André da Costa, Leila Ribeiro

Publication date 20 July 2012

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2010.02.006

zbMATH Keywords

theorem proving(attributed) graph grammarsrelational structures

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formal verification of graph grammars using mathematical induction
• Theorem proving graph grammars with attributes and negative application conditions
• CONCUR 2004 - Concurrency Theory
• Verifying a behavioural logic for graph transformation systems
• Process specification and verification

Cites work

• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 710624 (Why is no real title available?)
• scientific article; zbMATH DE number 2016064 (Why is no real title available?)
• scientific article; zbMATH DE number 1437942 (Why is no real title available?)
• A framework for the verification of infinite-state graph transformation systems
• Computer Aided Verification
• Computer Aided Verification
• Developments in Language Theory
• Formal Methods for the Design of Real-Time Systems
• Formal verification of graph grammars using mathematical induction
• Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories
• Graph Transformations
• Handbook of Graph Grammars and Computing by Graph Transformation
• Modeling and verifying graph transformations in proof assistants
• Monadic second-order definable graph transductions: a survey
• On the Use of Alloy to Analyze Graph Transformation Systems
• Symbolic model checking with rich assertional languages
• Towards attributed graphs in Groove (work in progress)
• Towards the Verification of Attributed Graph Transformation Systems
• Unfolding semantics of graph transformation
• Verification of distributed object-based systems.

Cited in

(15)

• Verifying object-based graph grammars
• Specification patterns for properties over reachable states of graph grammars
• A Temporal Graph Logic for Verification of Graph Transformation Systems
• Incorrectness logic for graph programs
• Theorem proving graph grammars: strategies for discharging proof obligations
• Formal verification of object-oriented graph grammars specifications
• Formal verification of graph grammars using mathematical induction
• Interactive and automated proofs for graph transformations
• CONCUR 2004 - Concurrency Theory
• Theorem proving graph grammars with attributes and negative application conditions
• Rule-based transformation of graph rewriting rules: towards higher-order graph grammars
• Logical description of context-free graph languages
• Translating controlled graph grammars to ordinary graph grammars
• Verigraph: a system for specification and analysis of graph grammars
• Process specification and verification

Describes a project that uses

Uses Software

• SPIN
• AGG
• Uppaal
• GROOVE

This page was built for publication: Verification of graph grammars using a logical approach

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