The Use of Theorem Provers in the Teaching and Practice of Formal Methods

Our aim is to make formal methods, in particular that which has to do with proving properties of programs, more accessible. Our immediate objective is the provision of usable tools by applying principles from HCI to the design of semi-automated theorem provers. In this paper we describe the XBarnacle semi-automated proof tool based on the CLAM proof planning system. This system is more powerful and more usable than the automated system on which it is based. The user can interact with the graphical user interface, which is in the form of a proof tree, directly, to redo steps or seek more information about the proof process. We have observed the use of the tool amongst both researchers and novice students of formal methods. A pilot evaluation has already taken place, and actively informs future development.