Extended static checking

  • Leino K
N/ACitations
Citations of this article
39Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free