Applications of Extended Static Checking
Abstract:
Extended static checking (ESC) is a technique for finding common
programming errors at compile time, including null dereferences,
array index bounds errors, type cast errors, race conditions, and
declared program invariants. The technique performs a detailed
semantical analysis of a given program module by translating each
method body into a mathematical formula that is analyzed by a
mechanical theorem prover. A user can supply light-weight
specifications, which are then used, and checked, by the ESC
tool.
In this talk, I will describe the extended static checking
technique and the ESC/Java checker. I will also discuss other
possible applications of ESC, for example to the automatic
inference of program properties and to the design of future
programming languages.
Program Analysis for Multithreaded Programs
Abstract:
The field of program analysis has focused primarily on languages
without explicit multithreading. But multithreading is becoming
increasingly important: as a program structuring mechanism, to
multiplex long latency events such as interactions with users and
network communications, and to support efficient parallel
computations. In this talk I will present several problems that arise
when attempting to generalize existing analysis frameworks to handle
multithreaded programs, and discuss how these problems may (or may
not) be resolved.
Language-based Security: What's needed and why
Abstract:
Language-based security leverages program analysis and program
rewriting in enforcing security policies. The approach promises
efficient enforcement of fine-grained access-control policies, and it
seems to require a trusted computing base of only modest size. This
talk discusses progress and prospects for the area. Traditional
security problems viewed through the lens of programming
language research invites novel uses of various well understood
results from the area. It also provides reason to revisit assumptions
and research directions that have been driving forces in languages
research.
K. Rustan M. Leino (Compaq SRC)
Martin C. Rinard (Massachusetts Institute of Technology)
Fred Schneider (Cornell University)