Formal verification of graph grammars using mathematical induction

DOI10.1016/J.ENTCS.2009.05.044MaRDI QIDQ5179351zbMATH OpenOpenAlexFDO

Authors Simone André da Costa, Leila Ribeiro

Publication date 19 March 2015

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.2009.05.044

zbMATH Keywords

formal verificationgraph grammarsmathematical induction

Mathematics Subject Classification ID

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

Recommendations

• Verification of graph grammars using a logical approach
• Verifying object-based graph grammars
• Theorem proving graph grammars with attributes and negative application conditions
• CONCUR 2004 - Concurrency Theory
• Process specification and verification

Cites work

• Developments in Language Theory
• Formal Methods for the Design of Real-Time Systems
• Formal Methods in Software and Systems Modeling
• Graph Transformations
• Handbook of automated reasoning. In 2 vols
• Handbook of Graph Grammars and Computing by Graph Transformation
• scientific article; zbMATH DE number 2016064 (Why is no real title available?)
• scientific article; zbMATH DE number 1569120 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• 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
• Unfolding semantics of graph transformation
• Verification of distributed object-based systems.

Cited in

(12)

• Formal verification of timed synchronous dataflow graphs using Lustre
• Inductive theorem proving based on tree grammars
• Theorem proving graph grammars with attributes and negative application conditions
• Verifying object-based graph grammars
• Formal verification of object-oriented graph grammars specifications
• Explicit State Model Checking for Graph Grammars
• Correct transformation: from object-based graph grammars to PROMELA
• Verification of graph grammars using a logical approach
• Interactive and automated proofs for graph transformations
• Process specification and verification
• Theorem proving graph grammars: strategies for discharging proof obligations
• Specification patterns for properties over reachable states of graph grammars

Describes a project that uses

Uses Software

• SPIN
• Isabelle/HOL

This page was built for publication: Formal verification of graph grammars using mathematical induction

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