2/25/2002
1:00pm-2:00pm
Clark
|
Type Qualifiers: Lightweight Specifications to Improve Software Quality
Department of Computer Science, University of California, Berkeley
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.
As part of my research I have built Cqual, a tool
for adding new type qualifiers to C. During the talk I will demonstrate two
applications of Cqual: finding format-string bugs,
a particular kind of security vulnerability, in C programs, and detecting
simple deadlocks in the Linux kernel. I will also discuss experiments in which
we found a number of format-string bugs and potential deadlocks.
More information about Cqual, including source code
and a web-based demonstration, can be found on the
Cqual website.
Hosted by Amer Diwan.
Refreshments will be served immediately following the talk in ECOT 831.
|
