SRC Research Report 159

Extended Static Checking

David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe

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.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 216 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 122 Kbytes
  
• PostScript compressed with ZIP -- 122 Kbytes
  
• PostScript -- 408 Kbytes
  
• Portable Document Format (PDF) -- 176 Kbytes