Static Analysis for Software Assurance: Soundness, Scalability and Adaptiveness

摘要

Standard approaches to software assurance are either process-based or test-based. We propose to include static analysis by Abstract Interpretation to the software development cycle. Static analysis by Abstract Interpretation provides a high level of assurance as well as ground-truth evidence in support of its findings. Successes in the verification of large industrial codes demonstrate the readiness of this technology. However, in order to be practical in real development environments, static analysis must be able to scale and yield few false positives without the need for expert hand-tuning. We present a research agenda to reach this goal based on the development of adaptive static analysis algorithms.