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

点击翻译按钮获取中文摘要

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.