SHF: Small: Collaborative Research: Mera: Memoized Ranged Systematic Software Analyses

SHF：小型：协作研究：Mera：记忆范围系统软件分析

• 批准号: 1319858
• 负责人: Corina Pasareanu
• 金额: $ 14.9万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-08-01 至 2017-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319858&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Mera

As software pervades our society and lives, failures due to softwarebugs become increasingly costly. Scalable approaches forsystematically checking software to find crucial bugs hold a key todelivering higher quality software at a lower cost. Mera is amethodology to scale model checking and symbolic execution which are twopowerful approaches for systematic software analysis and known to becomputationally expensive.The project builds on two novel concepts: memoization, which allowsre-using computations performed across different checks to amortizethe cost of software analysis; and ranging, which allows distributingthe analysis into sub-problems of lesser complexity, which can besolved separately and efficiently. Mera consists of three researchthrusts. First, the core memoization and ranging techniques for modelchecking and symbolic execution are developed. Second, thesetechniques are optimized in the context of different kinds of changes,like the program code, expected properties, or analysis search-depthparameters. Third, these techniques are adapted to effectivelyutilize available resources for parallel computation using static anddynamic strategies, such as work stealing. Mera will help improvesoftware quality and reliability thus holding the potential to providesubstantial economic benefits and to improve our quality of life.

随着软件弥漫在我们的社会和生活中，由于软件错误而导致的故障变得越来越昂贵。系统地检查软件以发现关键错误的可扩展方法是以较低成本交付更高质量软件的关键。MERA是一种扩展模型检查和符号执行的方法，这两种方法是系统软件分析的两种主要方法，但众所周知，这两种方法的成本很高。该项目建立在两个新概念的基础上：记忆化和测距。记忆化允许重复使用跨不同检查执行的计算来摊销软件分析的成本；测距允许将分析分配到复杂度较低的子问题中，这些子问题可以单独有效地解决。MERA由三个研究项目组成。首先，开发了用于模型检查和符号执行的核心记忆和测距技术。其次，这些技术在不同种类的更改的上下文中进行了优化，如程序代码、预期属性或分析搜索深度参数。第三，这些技术适用于使用静态和动态策略，如工作窃取，有效地利用可用资源进行并行计算。MERA将有助于提高软件质量和可靠性，从而具有提供实质性经济效益和改善我们的生活质量的潜力。