• DocumentCode
    1554606
  • Title

    A theorem prover for verifying iterative programs over integers

  • Author

    Sarkar, D. ; De Sarkar, S.C.

  • Author_Institution
    Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
  • Volume
    15
  • Issue
    12
  • fYear
    1989
  • fDate
    12/1/1989 12:00:00 AM
  • Firstpage
    1550
  • Lastpage
    1566
  • Abstract
    An implementation of a rule-based theorem prover for verifying iterative programs over integers is presented. The authors emphasize the overall proof construction strategy of the prover which has been able to construct the correctness proofs of all iterative programs taken from the literature. Two performance measures for the prover are proposed, and its proof construction for an array-sorting program is evaluated using these measures
  • Keywords
    expert systems; iterative methods; program verification; theorem proving; array-sorting program; correctness proofs; iterative programs; overall proof construction strategy; performance measures; rule-based theorem prover; Computer science; Humans; Programmable logic arrays; Sorting;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/32.58767
  • Filename
    58767
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1554606