Hoare-style verification of graph programs

DOI10.3233/FI-2012-708MaRDI QIDQ2898467zbMATH OpenOpenAlexFDO

Authors Christopher M. Poskitt, Detlef Plump

Publication date 11 July 2012

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2012-708

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• A Hoare calculus for graph programs
• Reasoning about graph programs
• Verifying graph programs with monadic second-order logic
• Verifying monadic second-order properties of graph programs
• The Graph Programming Language GP

Cited in

(22)

• Monadic second-order incorrectness logic for GP 2
• Incorrectness logic for graph programs
• Verifying graph programs with monadic second-order logic
• Theorem proving graph grammars with attributes and negative application conditions
• Translating essential OCL invariants to nested graph constraints focusing on set operations
• A Hoare-like calculus using the \(\mathrm{SROIQ}^{\sigma }\) logic on transformations of graphs
• Verifying monadic second-order properties of graph programs
• Tool-Based Verification of a Relational Vertex Coloring Program
• The Graph Programming Language GP
• Interactive and automated proofs for graph transformations
• A Hoare calculus for graph programs
• scientific article; zbMATH DE number 1390250 (Why is no real title available?)
• Reasoning about graph programs
• Analysis of graph transformation systems: native vs translation-based techniques
• scientific article; zbMATH DE number 7456057 (Why is no real title available?)
• Preserving consistency in geometric modeling with graph transformations
• From imperative to rule-based graph programs
• Graph Transformations
• Linear-time graph algorithms in GP 2
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• Decidability of Resilience for Well-Structured Graph Transformation Systems
• Juggrnaut: using graph grammars for abstracting unbounded heap structures

Describes a project that uses

Uses Software

• GrGen

This page was built for publication: Hoare-style verification of graph programs

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