Verifying the Absence of Common Runtime Errors in Computer Programs
Abstract
The Runcheck verifier is a working prototype system for proving the absence of runtime errors such as arithmetic overflow, array subscripting out of range, accessing an uninitialized variable, and dereferencing a null pointer. Such errors cannot be detected at compile time by most compilers. Runcheck accepts Pascal programs documented with assertions and proves that the assertions are consistent with the program and that no runtime errors can occur.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1981
- Accession Number
- ADA109433
Entities
People
- Steven M. German
Organizations
- Stanford University