CAREER: Cascade -- Precision on Demand for Software Verification

点击翻译按钮获取中文摘要

Formal static analysis is an approach which has great potential for improving the reliability of computer systems. One of the key techniques used in static analysis is abstraction. There are many different kinds of abstractions, but they all have essentially the same goal: to achieve scalability by sacrificing precision. Unfortunately, abstraction leads to the possibility of false errors: scenarios in which a bug is reported even though there is no actual bug in the system.The main research hypothesis of this proposal is that many false errors can be eliminated by using a two-stage approach in which potential errors are subjected to further analysis by a tool whose focus is precision rather than abstraction. The second-stage tool provides precision on demand for a small and specific set of potential errors. The research will focus on novel techniques for precise analysis, performance, and scalability. These will be implemented and evaluated in the context of the Cascade tool: a fast, robust, and automatic tool providing precision on demand for static analysis of software.