Cornell Department of Computer Science Colloquium
4:15pm Thursday, September 13, 2001
B17 Upson Hall

Static Program Analysis via 3-Valued Logic

Tom Reps
University of Wisconsin

Dataflow analysis, abstract interpretation, and model checking are all concerned with the problem of exploring a program's behavior for all possible inputs, but without actually running the program on specific inputs. In all three domains, one of the major challenges is how to handle programs that use dynamically allocated storage -- a feature found in all modern programming languages, including C, C++, and Java. In programs written in such languages, a program's data structures can grow and shrink dynamically, with no fixed upper bound on their size or number. The analysis problem is complicated even more by the fact that such languages also permit fields of dynamically allocated objects to be destructively updated. In the case of thread-based languages, such as Java, the number of threads can also grow and shrink dynamically -- again with no fixed upper bound on size or number.

A key technical challenge is to find a way to create finite-sized descriptors of memory configurations. Such descriptors must abstract away certain details of the memory configurations that can possibly arise during execution, but must retain enough key information so that the analysis can identify interesting properties that hold. This talk presents a recently developed framework for static program analysis that addresses these issues by using 3-valued logic in a novel way.

(Joint work with M. Sagiv, R. Wilhelm, and E. Yahav.)

Host:  Greg Morrisett