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.

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