Reasoning about Graph Programs
Detlef Plump (The University of York, United Kingdom)
TL;DR
This paper demonstrates how the GP 2 graph programming language's simple syntax and semantics enable formal reasoning, including proofs of termination and correctness, through four case studies.
Contribution
It introduces a framework for program verification in GP 2 using graph transformation rules and induction, enhancing formal reasoning capabilities.
Findings
Successful proofs of termination and correctness in case studies
GP 2's simplicity facilitates formal reasoning
Framework supports verification of graph programs
Abstract
GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with four case studies how programmers can prove termination and partial correctness of their solutions. We argue that GP 2's graph transformation rules, together with induction on the length of program executions, provide a convenient framework for program verification.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.