The soundness of bugs is what matters (position statement)

Patrice Godefroid
[Google Scholar] [DBLP] [Citeseer]
Read: 27 August 2020

Proceedings of BUGS 2005 (PLDI 2005 Workshop on the Evaluation of Software Defect Detection Tools)
Chicago, IL, USA
June 2005
Note(s): symbolic execution, under-approximation
Papers: xie:bugs:2005

This one-page, position paper is “written in a provocative style for entertainment purposes” but, nevertheless, makes some very good points. The main argument is that the goal of most verification research is defect detection and that they should therefore focus on finding “sound bugs” (bugs that can actually occur) and avoid “unsound bugs” (false alarms). This is why (despite its limitations) testing remains so important: testing finds sound bugs. The solution is to switch from “may analysis” (over-approximation) to “must analysis” (under-approximation).

This paper is worth reading alongside xie:bugs:2005 (from the same workshop) that uses “soundness” in the more conventional sense of showing absence of any bugs of a certain class.


Over-approximation