SAGe: A Sound Static Analyzer for Wide-Spectrum Value Extraction

The high-level goal of the work proposed here is to further develop a new, sound static analyzer and weave it into an existing software development framework in order to support the production of high assurance software. More specifically: - The tool will be based on the Code Hawk source code analysis engine. Code Hawk uses the mathematical technique of abstract interpretation to accurately determine potential variable values (including pointers). Code Hawk uses state of the art algorithms, customizability, and careful engineering to achieve analysis effiency and precision. Code Hawk has been used to perform sophisticated analysis of deployed open source code. - The tool will be integrated into the Eclipse platform. Eclipse is a widely used open development platform comprised of extensible frameworks, tools, and runtimes for building, deploying, and managing software across the lifecycle. It includes components for developing software in various languages, and incorporates a framework for testing. - The tool will support lightweight verification, testing, and program understanding activities and will be based on a testing metaphor. Users will be able to specify input conditions (values, value ranges, initialization code, and usage scenarios) and expected outputs. In addition, the tool will make available the results of analysis in a form that will facilitate reasoning about the analyzed code. There will be no a priori constraints on which inputs or outputs may be specified. There will be no a priori constraints on the granularity of analysis (it may operate at the unit, subsystem, or whole program level). This tool will serve a number of constituencies. For developers and testers it will function like traditional testing, only better, providing more information of guaranteed quality. For verifiers it will provide select information of chosen granularity. For concerned customers it can be applied after development (on open source, say). It will not require modification of the source, unlike annotation-based verification, nor a changed development process.