Modular Analysis of Higher-Order Languages

Detecting bugs before releasing software is a major goal of software engineering. While a rigorous software development process and systematic testing help, only formal methods can guarantee the absence of bugs, or at least the absence of some classes of bugs. From sound type systems to theorem provers, such formal systems have been available for a long time, but the adoption of these advanced systems has been slow, due to both their inherent complexity and their sometimes poor running times.

My research focuses on static analyses for higher-order languages, in particular value-flow analyses for the Scheme programming language. The challenge is to create an analysis that is modular (so programmers can analyze individual modules even when the source code of the whole program is not available), fast, and precise (not too many false positives). Using a graphical static debugger based on such an analysis, programmers can view sound approximations of the values and errors that each expression in a program might produce at runtime, as well as view the flows of the values in the program. With this information, programmers can then easily trace the sources of bugs in an intuitive manner.