CAREER: Cascade -- Precision on Demand for Software Verification

形式静态分析是一种在提高计算机系统可靠性方面具有巨大潜力的方法。静态分析中使用的关键技术之一是抽象。有许多不同类型的抽象，但它们基本上都有一个相同的目标：通过牺牲精确度来实现可伸缩性。不幸的是，抽象会导致错误的可能性：在这种情况下，即使系统中没有实际的错误，也会报告错误。该建议的主要研究假设是，通过使用两阶段方法可以消除许多错误，其中潜在错误由专注于精度而不是抽象的工具进行进一步分析。第二阶段工具按需提供针对一组小而具体的潜在误差的精度。研究将集中在精确分析、性能和可扩展性的新技术上。这些将在Cascade工具的背景下实施和评估：Cascade工具是一种快速、强大和自动化的工具，可按需提供软件静态分析的精度。

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.