CRII: SHF: Scaling Systematic Software Analyses Using Memoization

CRII：SHF：使用记忆化扩展系统软件分析

• 批准号: 1464123
• 负责人: Guowei Yang
• 金额: $ 17.5万
• 依托单位: Texas State University - San Marcos
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-06-01 至 2019-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1464123&HistoricalAwards=false
• 关键词: CRII; SHF; Scaling; Systematic; Software

Systematic software analyses, such as model checking and symbolic execution, perform systematic exploration of program behaviors to find faults in software systems. While the usefulness of systematic software analyses for improving software reliability has long been established, scaling them to real-world applications remains a key technical challenge, since the state spaces of these applications typically are large and computationally expensive to explore systematically. This project develops a memoization-based approach to enhance scalability of systematic analyses. Specifically, the analysis results are re-used to amortize the cost of analysis over multiple successive executions of the analysis. The project investigates foundations that provide the basic tool-set for enabling reuse of analysis results, optimizations that specialize memoized analyses in the context of change, and the use of parallel techniques to effectively utilize the available computing resources. The technical contributions of the project could significantly enhance the efficacy of systematic analyses, which could have a broad impact by improving the quality of software systems.

系统的软件分析，例如模型检查和符号执行，对程序行为进行系统探索，以在软件系统中查找故障。尽管长期以来已经建立了系统软件分析来提高软件可靠性的有用性，但将它们扩展到现实世界中的应用程序仍然是一个关键的技术挑战，因为这些应用程序的状态空间通常很大，并且系统地探索的计算量很高。该项目开发了一种基于回忆化的方法来增强系统分析的可扩展性。具体而言，重新使用分析结果，以通过多次连续执行分析来摊销分析成本。该项目调查了基础，这些基金会提供了基本工具集，以实现分析结果的重复使用，在变化背景下专门进行记忆分析的优化以及使用并行技术有效地利用可用的计算资源。该项目的技术贡献可以显着提高系统分析的功效，这可能通过提高软件系统的质量而产生广泛的影响。