As software pervades our society and lives, failures due to software bugs become increasingly costly. Scalable approaches for systematically checking software to find crucial bugs hold a key to delivering higher quality software at a lower cost. Mera is a methodology to scale model checking and symbolic execution which are two powerful approaches for systematic software analysis and known to be computationally expensive.
The project builds on two novel concepts: memoization, which allows re-using computations performed across different checks to amortize the cost of software analysis; and ranging, which allows distributing the analysis into sub-problems of lesser complexity, which can be solved separately and efficiently. Mera consists of three research thrusts. First, the core memoization and ranging techniques for model checking and symbolic execution are developed. Second, these techniques are optimized in the context of different kinds of changes, like the program code, expected properties, or analysis search-depth parameters. Third, these techniques are adapted to effectively utilize available resources for parallel computation using static and dynamic strategies, such as work stealing. Mera will help improve software quality and reliability thus holding the potential to provide substantial economic benefits and to improve our quality of life.
