Title: Extended static checking

Abstract:

The Extended Static Checker (ESC) is a researach prototype system for
detecting at compile time certain programming errors that are normally
not detected until run time, and sometimes not even then.  For
example, ESC detects array bounds errors, NIL dereferences, and race
conditions and deadlocks in multi-threaded programs.

The implementation of ESC is essentially the same as the classical
implementation of a program verifier.  A verification condition (VC)
generator takes in annotated programs and produces VCs, which assert
that the program is consistent with its annotations and free of the
class of errors under consideration.  The VCs are given to an
automatic theorem prover.  Failed proofs lead to error messages.
Like a program verifier, ESC requires the programmer to annotate
procedure declarations with preconditions and postconditions, but the
annotations are generally less onerous than those that would be
required for a full functional correctness proof. ESC checking is
essentially automatic. ESC reports errors by line number, and it feels
to the programmer more like a type checker than like a theorem-prover.

The ESC research group at the DEC/Compaq/HP Systems Research Center
have built two ESC prototypes:  ESC/Modula-3 [0] and ESC/Java [2]. The
talk focuses on those lessons learned in the ESC project that seem
relevant to the grand challenge of a verifying compiler, including new
annotation techniques (used in ESC/Modula-3) to achieve modular
soundness for programs that use both data abstraction and information
hiding [3] and new automatic theorem-proving techniques (used in both
checkers) appropriate for program checking [1].

We also learned that it is important to focus on the scientific
problem (and not, for example, on the related educational and
marketing problems).

The talk will include a demonstration of ESC/Java, weather permitting.

[0] David Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe.
Extended Static Checking.
SRC Research Report 159,  Compaq Systems Research Center, Palo Alto
California, December 18, 1998. Available from the web site http: //
www. hpl. hp. com /techreports /Compaq-DEC.

[1] David Detlefs, Greg Nelson, and James B. Saxe.
Simplify: an automatic theorem-prover for program checking.
HP Laboratories Technical Report HPL-2003-148, July 16th 2003.
Available from http: //www. hpl. hp. com /techreports.  To appear in JACM.

[2] Cormac Flanagan, Rustan Leino, Mark Lillibridge, Greg Nelson, and Raymie
Stata.
Extended Static Checking for Java.
Proceedings of the ACM PLDI Conference, June 2002,  Berlin, pp 234--45.

[3] K. Rustan M. Leino and Greg Nelson.
Data Abstraction and Information Hiding.
ACM TOPLAS Oct 2002. (Also appeared
as SRC Research Report 160, November, 2000, available from the HP labs
technical report web site.)