Dark Corners

Sound static program analysis promises exhaustive detection of many classes of program errors and, ideally, verification that the program is free of these errors. However, the critical issue is the lack of precision that such analyses inevitably encounter when analyzing the programs that occur in practice. Our hypothesis is that, in existing programs, only a small percentage of the code is responsible for the lack of precision for verification tasks. 

For Dark Corners, Aarno Labs developed program analysis tools that identify and mitigate the sources of imprecision in large, real-world programs. Our program analysis technologies identify the exact source of imprecision in the implementation using techniques such as logical abduction. Furthermore, our techniques increase precision once target code is identified, such as (1) Applying more expensive analysis techniques to this code; (2) Making manual changes to the code and/or adding annotations/dynamic checks to reduce the complexity; (3) Replacing the code with similar code from other implementations automatically; (4) Providing an alternative implementation that is easier to analyze but can be shown to match the existing implementation (with respect to memory safety).