Below, we compare our work to efforts in high-level compilation, verification, and extensible compilers. Many projects have hard wired application-level information in compilers. These projects use compiler support to analyze specific problems, whereas MC explicitly argues for the general use of compilers to check and optimize systems and provides an extensible framework for doing so. This extensibility enables detection of rule violations that are impossible to find without system-specific knowledge. Systems for finding software errors.
Verification uses stronger analysis than MC extensions.
However, MC extensions appear to be more generally effective. Verification's lower bug counts seem largely due to the difficulty in writing specifications, which scales with code size. As a consequence, only small pieces of code are verified. Both of these systems use stronger analyses than our approach. Their lack of extensibility means that, with the exception of ESC's support for finding some class of race conditions, neither system can find the system-level errors that MC can detect.