• DocumentCode
    1383853
  • Title

    A functional correctness model of program verification

  • Author

    Zelkowitz, Marvin V.

  • Author_Institution
    Dept. of Comput. Sci., Maryland Univ., College Park, MD, USA
  • Volume
    23
  • Issue
    11
  • fYear
    1990
  • Firstpage
    30
  • Lastpage
    39
  • Abstract
    A model whose verification conditions depend only on elementary symbolic execution of a trace table is presented. The method is applied to rather simple programs. However, even in large complex implementations, the techniques can be applied informally to determine the functionality of complex interactions. The technique is easy to learn (it is used in a freshman computer science course) and lends itself to automation.<>
  • Keywords
    program verification; elementary symbolic execution; functional correctness model; program verification; trace table; Computer bugs; Computer errors; Computer science; Design methodology; Education; Object oriented modeling; Software quality; Specification languages; Testing; Watches;
  • fLanguage
    English
  • Journal_Title
    Computer
  • Publisher
    ieee
  • ISSN
    0018-9162
  • Type

    jour

  • DOI
    10.1109/2.60878
  • Filename
    60878