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 at: http://www.cs.berkeley.edu/~jfoster/cqual