Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

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

    1st Irish Workshop on Formal Methods

    Dublin, Ireland. 3rd - 4th July 1997


    H. Lowe


    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.


    PDF filePDF Version of this Paper (61kb)