1,714
views
0
recommends
+1 Recommend
1 collections
    0
    shares

      Studying business & IT? Drive your professional career forwards with BCS books - for a 20% discount click here: shop.bcs.org

      scite_
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Proof and Refutation in Formal Software Development

      Published
      proceedings-article
      ,
      3rd Irish Workshop on Formal Methods (IWFM)
      Formal Methods
      1st - 2nd July 1999
      Bookmark

            Abstract

            In this paper we describe investigations into the use of automatic theorem proving technology in the refutation of proof obligations. Specifically, we discuss the use of resolution based theorem proving and model checking to find false obligations and counterexamples. These techniques can be used as basis of an automatic method for finding faults in design during the formal development of software. This approach is complementary to verifcation by proof as such proofs can only be completed when all faults have been corrected. We give a simple example using the B formal development method to demonstrate its potential.

            Content

            Author and article information

            Contributors
            Conference
            July 1999
            July 1999
            : 1-15
            Affiliations
            [0001]Information Technology Department

            Rutherford Appleton Laboratory

            Chilton, Didcot, Oxfordshire, OX11 OQX, UK.
            Article
            10.14236/ewic/IWFM1999.1
            301b482c-5692-437e-bab8-9f832b9f67ee
            © Juan C. Bicarregui et al. Published by BCS Learning and Development Ltd. 3rd Irish Workshop on Formal Methods

            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/

            3rd Irish Workshop on Formal Methods
            IWFM
            3
            Galway, Ireland
            1st - 2nd July 1999
            Electronic Workshops in Computing (eWiC)
            Formal Methods
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/IWFM1999.1
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction

            Comments

            Comment on this article