Theory and Practice of Mechanized Software Analysis

As software systems become ever more vital to all aspects of daily life, the risks posed by defects in critical software become increasingly dire. Traditional software engineering techniques focus heavily on manual analysis and testing to discover and repair defects. Although this approach is valuable, modern tools for the mechanized or automated detection of defects have proven themselves capable of alleviating much of the tedium associated with manual processes while providing greater assurance in their coverage. In this article, we describe the strengths and weaknesses of the most common approaches to the automated detection of software defects: formal methods and source code verification. We then describe our experience applying both free and commercial tools based on these techniques in the Software Analysis Research and Applications Laboratory (SARA Lab), a new effort at APL to enhance the state of the art in software analysis while applying best-of-breed tools for defect detection to APL software projects. APL software developers can avail themselves of this research by by e-mailing +SARALab.