An Extension of the Direct Method for Verifying Programs

dc.contributor.authorKang, Andy N. C.en
dc.contributor.authorWang, Shih-Hoen
dc.contributor.departmentComputer Scienceen
dc.date.accessioned2013-06-19T14:37:12Zen
dc.date.available2013-06-19T14:37:12Zen
dc.date.issued1975en
dc.description.abstractA direct method based on a finite set of path formulas which describe the input-output relations of a given program can be used to verify programs containing no overlapping loops. One major difficulty in verifying programs with overlapping loops using the above method is that too many path formulas (possibly infinite) needed to be considered. In this paper, we circumvent the above difficulty by applying the concept of modularity. The idea is to divide a program with overlapping loops into several small modules so that each module contains no overlapping loop. This can always be achieved if the program is in structured form. Then the path formulas will be derived for each module. By combining the path formulas for the modules, one can further obtain the path formulas for the given program and then use them to verify the program.en
dc.format.mimetypeapplication/pdfen
dc.identifierhttp://eprints.cs.vt.edu/archive/00000802/en
dc.identifier.sourceurlhttp://eprints.cs.vt.edu/archive/00000802/01/CS75022-R.pdfen
dc.identifier.trnumberCS75022-Ren
dc.identifier.urihttp://hdl.handle.net/10919/20291en
dc.language.isoenen
dc.publisherDepartment of Computer Science, Virginia Polytechnic Institute & State Universityen
dc.relation.ispartofHistorical Collection(Till Dec 2001)en
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.titleAn Extension of the Direct Method for Verifying Programsen
dc.typeTechnical reporten
dc.type.dcmitypeTexten

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
CS75022-R.pdf
Size:
304.19 KB
Format:
Adobe Portable Document Format