Accession Number:

ADA038191

Title:

Implementation of an Array Bound Checker,

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1976-11-01

Pagination or Media Count:

38.0

Abstract:

A practical system to check the correctness of array accesses automatically before actually running programs has been implemented. The system does not require any modification to input programs in the form of assertions or user interaction to guide proofs. That is, the system generates assertions to prove, synthesizes loop invariants, and finally proves verification conditions without interation. A powerful proof strategy is invented which makes the time to check programs almost linear to the size of programs, yet the system can completely verify the correctness of array accesses of programs like tree sort and binary search with processing speed of about fifty lines per ten seconds. A three hundred line program example is also shown. Author

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE