The proposed project will focus on techniques and tools for high-precision static and dynamic analyses of software. Current static analyzers often suffer from a high spurious error ratio, while dynamic analysis tools generally provide only partial coverage of program executions. It will be studied how to build on techniques from program abstraction, model checking, and theorem proving, to improve this status quo. At its core, the proposal is to investigate the trade-off between the quality of the analysis results, and the computational effort needed to obtain them.
The broad impact will be to enable the creation of software that is more robust, with shorter development times. In addition, it is expected that the research will lead to a better scientific understanding of several core techniques. A key component of the proposal is to build effective tools that incorporate these research results. These tools will enable the application of our research ideas to the NASA testbed, and communicate them to the programming community at large. The research results are also expected to be communicated to the research community through conference and journal publications.
