Implementation of an Array Bound Checker,
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1976
- Accession Number
- ADA038191
Entities
People
- Kiyoshi Ishihata
- Norihisa Suzuki
Organizations
- Carnegie Mellon University