Rice Computer Science-Colloquia

Rice Computer Science-Colloquia Rice University
Department of Computer Science
presents

K. Rustan M. Leino

Digital Equipment Corporation

Extended Static Checking

Abstract

The Extended Static Checker (ESC) is a programming tool that works on object-oriented, concurrent programs to find programming errors like nil-dereference errors, array index out-of-bounds errors, deadlocks, and race conditions. To use the tool, a programmer annotates a program with simple specifications.

ESC works by transforming a program and its specifications into verification conditions (logical formulas) that are passed to an automatic theorem prover. The theory underlying these transformations has required the generalization of data abstraction.

ESC has been applied to, for example, Modula-3's object-oriented I/O streams library.

In this talk, I will give an overview and a demo of the ESC system.

Tuesday, July 29 @ 10 a.m. in Duncan Hall 1044
Reception to follow in 1044

Rustan Leino's home page