Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2014
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.
Keywords
Graph theory, graph transformations
Discipline
Theory and Algorithms
Research Areas
Software and Cyber-Physical Systems
Publication
Graph transformation: 7th International Conference, ICGT 2014, York, July 22-24, Proceedings
Volume
8571
First Page
33
Last Page
48
ISBN
9783319091082
Identifier
10.1007/978-3-319-09108-2_3
Publisher
Springer
City or Country
Berlin
Citation
POSKITT, Christopher M. and PLUMP, Detlef.
Verifying monadic second-order properties of graph programs. (2014). Graph transformation: 7th International Conference, ICGT 2014, York, July 22-24, Proceedings. 8571, 33-48.
Available at: https://ink.library.smu.edu.sg/sis_research/4912
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-319-09108-2_3