264
views
0
recommends
+1 Recommend
1 collections
    4
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

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

      proceedings-article

      Proceedings of the 1st Irish Workshop on Formal Methods (FM)

      Irish Workshop on Formal Methods

      3-4 July 1997

      Bookmark

            Abstract

            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.

            Content

            Author and article information

            Conference
            September 1997
            September 1997
            : 1-9
            Affiliations
            [0001]Department of Computing, Napier University

            Edinburgh, EH14 1DJ
            Article
            10.14236/ewic/FM1997.7
            ea5519e8-10b0-45ec-964d-7812878a5be3
            © Helen Lowe. Published by BCS Learning and Development Ltd. Proceedings of the 1st Irish Workshop on Formal Methods, Dublin

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Proceedings of the 1st Irish Workshop on Formal Methods
            FM
            1
            Dublin
            3-4 July 1997
            Electronic Workshops in Computing (eWiC)
            Irish Workshop on Formal Methods
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article