You might wonder what is the difference between the Cyclone project and a few other projects, notably LCLint from MIT and Virginia, the Extended Static Checking (ESC) project from Compaq SRC, and the Safe-C project from the University of Wisconsin. These are good systems and we have great respect for the work that has gone into them. But their goals are quite different from Cyclone and we view our work as somewhat overlapping, but mostly complementary.
Though we are interested in finding and eliminating bugs, we also want to guarantee a certain level of safety. LCLint can't provide such a guarantee, because the underlying language (C) and associated static analyses are unsound (i.e., some bugs will not be caught). The reason for this is that without changing C, it is extremely difficult to guarantee safety without a lot of extra runtime overhead, or a lot of false positives in your static analysis. LCLint is aimed at being a practical tool for debugging C code, and as such, makes compromises to eliminate false positives, but at the expense of soundness. Thus, LCLint can't be used in settings where security is a concern.
ESC is similar in some ways to LCLint, but is built on top of Java. (A previous version was built on top of Modula-3). Since Java and Modula-3 are type-safe, there is a fundamental safety guarantee provided by the ESC system. And in addition, one gets the extra (really amazing) bug-finding power of ESC. However, as we argued above, many systems programming tasks cannot be coded in languages such as Java (or Modula-3) or at least can't be coded efficiently. In addition, it is difficult to move legacy code written in C to these environments.
Consequently, we see the ESC and LCLint projects as complementary to the Cyclone project. Ideally, after Cyclone reaches a stable design point, we should be able to put an ``ESC/Cyclone'' or ``LCLint/Cyclone'' static debugging tool together.
The Safe-C project out of Wisconsin is perhaps the closest in spirit to ours, in that they are attempting to provide a memory-safety guarantee. However, the approach taken by Safe-C is quite different than Cyclone: Programs continue to be written in C, but extra indirections and dynamic checks are inserted to ensure that abstractions are respected. For example, pointers in Safe-C are actually rather complex data structures, and dereferencing a pointer is an expensive operation as a number of checks must be done to ensure that the pointer is still valid. In order to avoid some of these overheads, the Wisconsin folks apply sophisticated, automatic analyses.
The advantage of Safe-C is that, in principle, programs can be compiled and run with no modification by the programmer. The disadvantages are that (a) there is still a great deal of space and time overhead for programs, (b) the data representations change radically. As such, the whole system (e.g., the standard libraries) has to be recompiled and pieces of code cannot be migrated from C to Safe-C. In contrast, Cyclone goes to great lengths to preserve the data representations so that Cyclone and C code can smoothly interoperate. Furthermore, many more checks are performed statically in Cyclone. The downside is that programmers have to change the code (typically, by modifying or adding more typing information), and they can't always write what they want. Our research is aimed at eliminating these drawbacks and to compare against the Safe-C approach.