Problem
44 COMMUNICATIONS OF THE ACM | FEBRUARY 2015 | VOL. 58 | NO. 2 V viewpoints Viewpoint In Defense of Soundiness: A Manifesto Soundy is the new sound. dominant practice is one of treating soundness as an engineering choice. In all, we are faced with a paradox: on the one hand we have the ubiquity of unsoundness in any practical whole- program analysis tool that has a claim to precision and scalability; on the other, we have a research community that, outside a small group of experts, is oblivious to any unsoundness, let alone its preponderance in practice.
Approach
Our observation is that the paradox can be reconciled. The state of the art in realistic analyses exhibits consis tent traits, while also integrating a sharp discontinuity. On the one hand, S TATIC PROGRAM ANALYSIS is a key component of many software development tools, including compilers, devel opment environments, and verification tools. Practical applications of static analysis have grown in recent years to include tools by companies such as Coverity, Fortify, GrammaTech, IBM, and others. Analyses are often expected to be sound in that their result models all possible executions of the program under analysis.
Results
Soundness implies the analysis computes an over-approxima tion in order to stay tractable; the analy sis result will also model behaviors that do not actually occur in any program execution. The precision of an analysis is the degree to which it avoids such spurious results. Users expect analyses to be sound as a matter of course, and desire analyses to be as precise as pos sible, while being able to scale to large programs. Soundness would seem essential for any kind of static program analy sis. Soundness is also widely empha sized in the academic literature. Yet, in practice, soundness is commonly eschewed: we are not aware of a single realistic whole-programa analysis tool (for example, tools widely used for bug detection, refactoring assistance, p