Verifying monadic second-order properties of graph programs

DOI10.1007/978-3-319-09108-2_3MaRDI QIDQ3192221zbMATH OpenOpenAlexFDO

Authors Christopher M. Poskitt, Detlef Plump

Publication date 26 September 2014

Published in Graph Transformation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.5927, https://ink.library.smu.edu.sg/sis_research/4912

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: The core challenge in a Hoare- or Dijkstra-style proof system for graph programs is in defining a weakest liberal precondition construction with respect to a rule and a postcondition. Previous work addressing this has focused on assertion languages for first-order properties, which are unable to express important global properties of graphs such as acyclicity, connectedness, or existence of paths. In this paper, we extend the nested graph conditions of Habel, Pennemann, and Rensink to make them equivalently expressive to monadic second-order logic on graphs. We present a weakest liberal precondition construction for these assertions, and demonstrate its use in verifying non-local correctness specifications of graph programs in the sense of Habel et al.

Recommendations

• Verifying graph programs with monadic second-order logic
• Hoare-style verification of graph programs
• A Hoare calculus for graph programs
• Weakest Preconditions for High-Level Programs
• Two-level reasoning about graph transformation programs

Cited in

(19)

• Ensuring correctness of model transformations while remaining decidable
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• A navigational logic for reasoning about graph properties
• Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
• Weakest Preconditions for High-Level Programs
• Institutions for navigational logics for graphical structures
• Local reasoning for global graph properties
• Theorem proving graph grammars with attributes and negative application conditions
• A Hoare calculus for graph programs
• scientific article; zbMATH DE number 7649899 (Why is no real title available?)
• Hoare-style verification of graph programs
• Fly-automata for checking monadic second-order properties of graphs of bounded tree-width
• Reasoning about graph programs
• Towards mechanised proofs in double-pushout graph transformation
• On the operationalization of graph queries with generalized discrimination networks
• Reachability predicates for graph assertions
• Monadic second-order incorrectness logic for GP 2
• Incorrectness logic for graph programs
• Verifying graph programs with monadic second-order logic

This page was built for publication: Verifying monadic second-order properties of graph programs

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