SHF: Small: Dynamic Abstractions for Verification

验证是当前社会所依赖的硬件和软件系统设计的主要瓶颈。设计错误可能导致召回、软件崩溃、网络攻击，甚至是生命损失。识别和修复设计错误的基本方法是使用形式化验证，它检查一组系统属性是否跨越所有可能的系统行为。不幸的是，当前算法的可扩展性很差，不能直接应用于现代设计。这个缺点目前是通过使用手工抽象来解决的，这种抽象实质上隐藏了不相关的实现细节，从而减少了要分析的公式的大小。除了涉及的手工工作之外，这种方法的另一个缺点是很难保证抽象是正确的。提出的研究目标是开发有效的方法来构建可证明正确的抽象，从而大大提高形式化验证算法的可扩展性。我们找到正确抽象的方法基于以下三个想法。首先，在搜索空间的小子空间中构建一个正确的抽象是很容易的。第二，我们可以将子空间的抽象组合在一起，以产生到目前为止所探索的整个子空间的抽象。第三，为探索过的子空间构建的抽象可能适用于许多尚未访问过的子空间。这种抽象的可重用性使得我们的方法在识别公式的不相关部分方面非常强大。从理论的角度来看，提出的研究将导致对抽象的更好理解和新的形式化验证算法的发展。从实际的角度来看，它将导致创建各种工具，包括sat求解器和模型检查器，这将提高形式验证的可扩展性。

Verification is currently a major bottleneck in the design of thehardware and software systems society depends on. Design errorscan lead to recalls, software crashes, cyber attacks, and eventhe loss of life. A fundamental approach for identifying andfixing design errors is to use formal verification, which checkswhether a set of system properties holds across all possiblesystem behaviors. Unfortunately, current algorithms suffer frompoor scalability and cannot be directly applied to moderndesigns. This drawback is currently addressed with the use ofmanual abstractions that in essence hide irrelevantimplementation details, thereby reducing the size of formulas tobe analyzed. Besides the manual effort involved, anotherdisadvantage of this approach is that it is very hard toguarantee that an abstraction is correct. The goal of the proposedresearch is to develop efficient methods for algorithmicallybuilding provably correct abstractions, thereby drasticallyimproving the scalability of formal verification algorithms.Our approach to finding correct abstractions is based on thefollowing three ideas. First, building an abstraction that iscorrect in a small subspace of the search space is easy. Second,one can stitch together abstractions found for subspaces toproduce an abstraction for the entire subspace explored so far.Third, abstractions built for explored subspaces may hold in manysubspaces that have not been visited yet. This re-usability ofabstractions makes our approach extremely powerful in identifyingirrelevant parts of formulas. From a theoretical point of view,the proposed research will lead to a better understanding ofabstractions and to the development of new formal verificationalgorithms. From a practical point of view, it will result in thecreation of various kinds of tools including SAT-solvers and model checkers that will boost the scalability of formalverification.