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.