SAS'01 Invited Speakers

K. Rustan M. Leino     M. Rinard     Fred Schneider

K. Rustan M. Leino (Compaq SRC)

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.

Martin C. Rinard (Massachusetts Institute of Technology)

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.

Fred Schneider (Cornell University)

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.