Hoare logic for graph programs
We present a new approach for verifying programs written in GP (for Graph Programs), an experimental programming language for performing computations on graphs at a high level of abstraction. Taking a labelled graph as input, a graph program nondeterministically applies to it a number of graph trans...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2010
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/4921 https://ink.library.smu.edu.sg/context/sis_research/article/5924/viewcontent/PoskittPlump.VSTTE_Theory.2010.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| id |
sg-smu-ink.sis_research-5924 |
|---|---|
| record_format |
dspace |
| spelling |
sg-smu-ink.sis_research-59242020-02-13T06:54:35Z Hoare logic for graph programs POSKITT, Christopher M. PLUMP, Detlef We present a new approach for verifying programs written in GP (for Graph Programs), an experimental programming language for performing computations on graphs at a high level of abstraction. Taking a labelled graph as input, a graph program nondeterministically applies to it a number of graph transformation rules, directed by simple control constructs such as sequential composition and as-long-as-possible iteration. We adapt classical Hoare logic to the domain of graphs, and describe a system of sound proof rules for showing the partial correctness of graph programs. 2010-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4921 info:doi/10.3929/ethz-a-006860117 https://ink.library.smu.edu.sg/context/sis_research/article/5924/viewcontent/PoskittPlump.VSTTE_Theory.2010.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Theory and Algorithms |
| institution |
Singapore Management University |
| building |
SMU Libraries |
| continent |
Asia |
| country |
Singapore Singapore |
| content_provider |
SMU Libraries |
| collection |
InK@SMU |
| language |
English |
| topic |
Theory and Algorithms |
| spellingShingle |
Theory and Algorithms POSKITT, Christopher M. PLUMP, Detlef Hoare logic for graph programs |
| description |
We present a new approach for verifying programs written in GP (for Graph Programs), an experimental programming language for performing computations on graphs at a high level of abstraction. Taking a labelled graph as input, a graph program nondeterministically applies to it a number of graph transformation rules, directed by simple control constructs such as sequential composition and as-long-as-possible iteration. We adapt classical Hoare logic to the domain of graphs, and describe a system of sound proof rules for showing the partial correctness of graph programs. |
| format |
text |
| author |
POSKITT, Christopher M. PLUMP, Detlef |
| author_facet |
POSKITT, Christopher M. PLUMP, Detlef |
| author_sort |
POSKITT, Christopher M. |
| title |
Hoare logic for graph programs |
| title_short |
Hoare logic for graph programs |
| title_full |
Hoare logic for graph programs |
| title_fullStr |
Hoare logic for graph programs |
| title_full_unstemmed |
Hoare logic for graph programs |
| title_sort |
hoare logic for graph programs |
| publisher |
Institutional Knowledge at Singapore Management University |
| publishDate |
2010 |
| url |
https://ink.library.smu.edu.sg/sis_research/4921 https://ink.library.smu.edu.sg/context/sis_research/article/5924/viewcontent/PoskittPlump.VSTTE_Theory.2010.pdf |
| _version_ |
1770575095998185472 |