Automating Proofs of the Absence of Common Runtime Errors

Abstract

The Runcheck Verifier is a working system for proving the absence of common runtime errors. The language accepted is Pascal without variant records, side effects in functions, shared variable parameters to procedures, or functional arguments. The errors checked are: 1) accessing a variable that has not been assigned a value, 2) array subscripting out of range, 3) subrange type error, 4) dereferencing a NIL pointer, 5) arithmetic overflow, and 6) division by zero.