A graphical representation of verification proof plans

Yuhui Lin; Alan Bundy; Gudmund Grov

doi:10.1007/978-3-031-66676-6_15

A graphical representation of verification proof plans

Yuhui Lin, Alan Bundy^*, Gudmund Grov

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

Abstract / Description of output

We argue that the declarative, graphical and hierarchical representation of proofs, provided by proof plans, is a good vehicle for capturing the intentions of the person constructing the proof. It also assists other people in understanding the proof. This supports both the debugging of the proof and the reuse of generic proof plans in related proofs. We use PSGraphs to represent proof plans and the Tinker tool as a user interface. We evaluate the use of PSGraph on formal methods and verification proofs.

Original language	English
Title of host publication	The Practice of Formal Methods
Editors	A. Cavalcanti, J. Baxter
Publisher	Springer
Chapter	15
Pages	292-313
Number of pages	22
ISBN (Electronic)	9783031666766
ISBN (Print)	9783031666759
DOIs	https://doi.org/10.1007/978-3-031-66676-6_15
Publication status	Published - 4 Sept 2024

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	14780

Keywords / Materials (for Non-textual outputs)

formal method
theorem proving
proof plans

Access to Document

10.1007/978-3-031-66676-6_15

A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A., Bundy, A., Grov, G., Ireland, A. & Jones, C. B.
EPSRC
1/04/10 → 31/03/14
Project: Research

Cite this

@inbook{169320b331744c4f838e69a4fcb8e78b,

title = "A graphical representation of verification proof plans",

abstract = "We argue that the declarative, graphical and hierarchical representation of proofs, provided by proof plans, is a good vehicle for capturing the intentions of the person constructing the proof. It also assists other people in understanding the proof. This supports both the debugging of the proof and the reuse of generic proof plans in related proofs. We use PSGraphs to represent proof plans and the Tinker tool as a user interface. We evaluate the use of PSGraph on formal methods and verification proofs.",

keywords = "formal method, theorem proving, proof plans",

author = "Yuhui Lin and Alan Bundy and Gudmund Grov",

year = "2024",

month = sep,

day = "4",

doi = "10.1007/978-3-031-66676-6_15",

language = "English",

isbn = "9783031666759",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "292--313",

editor = "A. Cavalcanti and J. Baxter",

booktitle = "The Practice of Formal Methods",

address = "United Kingdom",

}

TY - CHAP

T1 - A graphical representation of verification proof plans

AU - Lin, Yuhui

AU - Bundy, Alan

AU - Grov, Gudmund

PY - 2024/9/4

Y1 - 2024/9/4

N2 - We argue that the declarative, graphical and hierarchical representation of proofs, provided by proof plans, is a good vehicle for capturing the intentions of the person constructing the proof. It also assists other people in understanding the proof. This supports both the debugging of the proof and the reuse of generic proof plans in related proofs. We use PSGraphs to represent proof plans and the Tinker tool as a user interface. We evaluate the use of PSGraph on formal methods and verification proofs.

AB - We argue that the declarative, graphical and hierarchical representation of proofs, provided by proof plans, is a good vehicle for capturing the intentions of the person constructing the proof. It also assists other people in understanding the proof. This supports both the debugging of the proof and the reuse of generic proof plans in related proofs. We use PSGraphs to represent proof plans and the Tinker tool as a user interface. We evaluate the use of PSGraph on formal methods and verification proofs.

KW - formal method

KW - theorem proving

KW - proof plans

U2 - 10.1007/978-3-031-66676-6_15

DO - 10.1007/978-3-031-66676-6_15

M3 - Chapter (peer-reviewed)

SN - 9783031666759

T3 - Lecture Notes in Computer Science

SP - 292

EP - 313

BT - The Practice of Formal Methods

A2 - Cavalcanti, A.

A2 - Baxter, J.

PB - Springer

ER -

A graphical representation of verification proof plans

Abstract / Description of output

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

A14FM : using A1 to aid automation of proof search in formal methods

Cite this