A Graphical Representation of Verification Proof Plans

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.