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

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

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)

• Reachability predicates for graph assertions
• A navigational logic for reasoning about graph properties
• 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
• Hoare-style verification of graph programs
• Ensuring correctness of model transformations while remaining decidable
• On the operationalization of graph queries with generalized discrimination networks
• Fly-automata for checking monadic second-order properties of graphs of bounded tree-width
• Weakest Preconditions for High-Level Programs
• A Hoare calculus for graph programs
• Reasoning about graph programs
• Local reasoning for global graph properties
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Linear-time graph algorithms in GP 2
• Towards mechanised proofs in double-pushout graph transformation
• Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
• Institutions for navigational logics for graphical structures

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)