My research goal is to develop tractable analyses and representations for software. An analysis is tractable if it can be done mechanically without exorbitant resources; a representation is tractable if it admits tractable analysis, and in addition, can be constructed and manipulated by hand without an inordinate amount of effort. Type declarations, for example, are tractable: they can be checked efficiently and are easily read and written by programmers. Formal specifications, on the other hand, are often intractable: they cost a lot to write, may be hard to read and even their simplest properties cannot be determined automatically.
Most developers cannot afford the cost of intractability, so they are led to abandon expressive representations in favour of extremely weak one - type systems, dataflow diagrams, call graphs, etc. - which cannot support the analyses called for by most development tasks, such as bug detection, reverse engineering and determining the effect of modifications. This is hardly surprising, as most static analysis techniques were not designed for these tasks at all, but for compiler optimization instead.
I think we need new representations and analyses, designed expressly for software engineering tasks. I am working primarily on two fronts, each characterized by one form of abstraction:
Dataflow dependences. I have developed a scheme for detecting bugs in code by writing partial specifications that can be checked by standard dependency analysis. A variant of the same technique can be used to find semantic differences between two versions of a program. My current project is the construction (with Gene Rollins) of a browsing editor for C programs that provides novel search and query functions based on these ideas.
State space partitioning. The idea of representing state machines in terms of transitions on equivalence classes of states rather than individual states is hardly new, but I believe it still offers much to be exploited. I am developing a model checking method for analyzing Z specifications that can handle infinite state spaces. The state abstraction trades precision for tractability; it may fail to prove a true theorem, but never proves a false one.
[Jackson and Ladd 94]
Daniel Jackson and David A. Ladd, ``Semantic Diff: A Tool for Summarizing the Effects of Modifications,'' submitted to International Conference on Software Maintenance, Victoria, BC, Canada, Sept. 1994.[Jackson 94]
Daniel Jackson, ``Abstract Model Checking of Infinite Specifications,'' submitted to FME'94, Barcelona, Sept. 1994.[Jackson 93]
Daniel Jackson, ``Abstract Analysis with Aspect,'' International Symposium on Software Testing and Analysis, Cambridge, MA, June 1993.