The paper describes a mechanical checker for software that catches many common programming errors, in particular array index bounds errors, nil dereference errors, and synchronization errors in multi-threaded programs. The checking is performed at compile-time. The checker uses an automatic theorem-prover to reason about the semantics of conditional statements, loops, procedure and method calls, and exceptions. The checker has been implemented for Modula-3. It has been applied to thousands of lines of code, including mature systems code as well as fresh untested code, and it has found a number of errors.
CITATION STYLE
Leino, K. R. M. (1998). Extended static checking. In Programming Concepts and Methods PROCOMET ’98 (pp. 1–1). Springer US. https://doi.org/10.1007/978-0-387-35358-6_1
Mendeley helps you to discover research relevant for your work.