Type Qualifiers: Lightweight Specifications to Improve Software Quality

Dr. Jeff Foster

University of Maryland

Friday, March 26, 2004
10:00am - SENSQ 5317
Refreshments at 9:30am in SENSQ 5319

Abstract

Software continues to increase in size and complexity, yet programmers have few practical tools and techniques to ensure its quality. In this talk I will discuss type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. I will describe efficient type qualifier inference algorithms, including a lazy, constraint-based flow-sensitive inference algorithm that explicitly models pointers, heap-allocated data, and aliasing. I will also present a language construct called restrict, based on the new ANSI C type qualifier of the same name, that allows us to regain local non-aliasing information, which can be used to improve the precision of flow-sensitive type qualifier inference and can also be adapted to other flow-sensitive analyses.

As part of my research I have built cqual, a tool for adding new type qualifiers to C. During the talk I will discuss several applications of cqual, including finding format-string bugs, a particular kind of security vulnerability, in C programs, and detecting simple deadlocks in the Linux kernel.

Joint work with Tachio Terauchi, John Kodumal, and Alex Aiken.

Bio Sketch

Jeff Foster is an Assistant Professor in the Department of Computer Science at the University of Maryland, College Park. He received his Ph.D. in Computer Science from the University of California, Berkeley, and he received M.Eng. and B.S. degrees from Cornell University, also in Computer Science. Jeff's research focuses on programming languages with applications to software engineering. In particular, he has studied advanced static type systems, alias analysis, and constraint-based analysis.