SHF: Small: Dynamic Abstractions for Verification

SHF：小型：用于验证的动态抽象

• 批准号: 1319580
• 负责人: Panagiotis Manolios
• 金额: $ 45万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319580&HistoricalAwards=false
• 关键词: SHF; Small; Dynamic; Abstractions; Verification

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.

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