A Hoare Calculus for Graph Programs

We present Hoare-style axiom schemata and inference rules for verifying the partial correctness of programs in the graph programming language GP. The pre- and postconditions of this calculus are the nested conditions of Habel, Pennemann and Rensink, extended with expressions for labels in order to deal with GP's conditional rule schemata and infinite label alphabet. We show that the proof rules are sound with respect to GP's operational semantics.

• Publication year

  2010

• Venue

  International Conference on Graph Transformation

• Publication date

  2010-09-27

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-642-15928-2_10
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The Semantics of Graph Programs

  2010influential reference
• A Hoare Calculus for Graph Programs (Long Version)

  2010cited by this paper
• Compositional Verification of Architectural Refactorings

  2009cited by this paper
• The Graph Programming Language GP

  2009influential reference
• Algebraic Informatics

  2009cited by this paper
• Correctness of high-level transformation systems relative to nested conditions†

  2009influential reference
• Towards the Verification of Attributed Graph Transformation Systems

  2008cited by this paper
• A framework for the verification of infinite-state graph transformation systems

  2008cited by this paper
• GrGen: A Fast SPO-Based Graph Rewriting Tool

  2006cited by this paper
• Weakest Preconditions for High-Level Programs

  2006cited by this paper
• Theories for the Global Ubiquitous Computer

  2004cited by this paper
• Applications of Graph Transformations with Industrial Relevance

  2004cited by this paper
• Model Checking Graph Transformations: A Comparison of Two Approaches

  2004cited by this paper
• AGG: A Graph Transformation Environment for Modeling and Validation of Software

  2003cited by this paper
• Architecting dependable systems

  2003cited by this paper
• Relabelling in Graph Transformation

  2002influential reference
• Computational Completeness of Programming Languages Based on Graph Transformation

  2001cited by this paper
• The FUJABA environment

  2000cited by this paper
• The PROGRES approach: language and environment

  1999cited by this paper
• Verification of Sequential and Concurrent Programs

  1997influential reference
• An axiomatic basis for computer programming

  1969influential reference
• Proceedings of the Seventh International Workshop on Graph Transformation and Visual Modeling Techniques (gt-vmt 2008) the Gp Programming System Greg Manning and Detlef Plump 13 Pages the Gp Programming System

  year unknowncited by this paper

• Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems (Full Version)

  2025cites this paper
• Inferring Data Preconditions from Deep Learning Models for Trustworthy Prediction in Deployment

  2024cites this paper
• A Strict Constrained Superposition Calculus for Graphs

  2023cites this paper
• A Superposition-Based Calculus for Diagrammatic Reasoning

  2021cites this paper
• Verifying Graph Programs with First-Order Logic (Extended Version)

  2020cites this paper
• Concurrent

  2020cites this paper
• Institutional Knowledge at Singapore Management University Institutional Knowledge at Singapore Management University A Hoare calculus for graph programs A Hoare calculus for graph programs

  2020cites this paper
• Verifying Graph Transformation Systems with Description Logics

  2018cites this paper
• On the Verification of Logically Decorated Graph Transformations

  2018cites this paper
• Applied Graph Transformation and Verification With Use Cases in Malaria Surveillance

  2018cites this paper
• A Semi-automatic Proof of Strong Connectivity

  2017cites this paper
• Hoare-like verification of graph transformation

  2016cites this paper
• Formal Verification of Relational Model Transformations using an Intermediate Verification Language

  2016cites this paper
• Ensuring Correctness of Model Transformations While Remaining Decidable

  2016cites this paper
• Towards Testing Model Transformation Chains Using Precondition Construction in Algebraic Graph Transformation

  2014cites this paper
• $\mathcal{M}$-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation

  2014cites this paper
• ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems

  2014influential citation
• Hoare-Style Verification of Graph Programs

  2012cites this paper
• Graph Transformations for MDE, Adaptation, and Models at Runtime

  2012cites this paper
• Formal Methods for Model-Driven Engineering

  2012cites this paper
• Verification of Graph Programs

  2012cites this paper
• Conditional Reactive Systems

  2011cites this paper
• Towards the Verification of Graph Programs Qualifying Dissertation

  2010cites this paper
• Hoare Logic for Graph Programs

  2010cites this paper
• VSTTE 2010 workshop proceedings

  2010influential citation
• Towards the Verification of Graph Programs

  2010cites this paper
• Using Graph Transformations and Graph Abstractions for Software Verification

  2009cites this paper