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

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

• 批准号: 1319688
• 负责人: Sarfraz Khurshid
• 金额: $ 35万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-08-01 至 2018-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319688&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将有助于提高软件质量和可靠性，从而保持提供巨大经济效益和提高我们生活质量的潜力。