Current type checking software is able to locate code that violates a given rule, but the software is extremely limited in its ability to provide evidence as to why the rule was violated. Knowing why a rule was violated is the first step in creating a viable solution or preventing code from violating the rule again in the future. Additionally, current type checking software can return bloated results for a rule violation, making it difficult to locate the exact portion of code causing the violation.
There is a need for a type checking software that:
- Leverages an existing analysis framework so that a complex tool can be built within a year as opposed to several years of effort (referencing the University of Washington Checker Framework project that this software is intended to improve upon)
- Provides useful approximate analysis (as the exact program analysis is known to be intractable)
- Provides powerful analysis capabilities incrementally, by refining the approximate analysis.