Verifying monadic second-order properties of graph programs
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 exp...
Saved in:
Main Authors: | POSKITT, Christopher M., PLUMP, Detlef |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2014
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4912 https://ink.library.smu.edu.sg/context/sis_research/article/5915/viewcontent/PoskittPlump.ICGT.2014.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
Similar Items
-
Verifying total correctness of graph programs
by: POSKITT, Christopher M., et al.
Published: (2012) -
Verification of graph programs
by: POSKITT, Christopher M.
Published: (2012) -
Monadic second-order incorrectness logic for GP 2
by: POSKITT, Christopher M., et al.
Published: (2023) -
A Hoare calculus for graph programs
by: POSKITT, Christopher M., et al.
Published: (2010) -
Hoare logic for graph programs
by: POSKITT, Christopher M., et al.
Published: (2010)