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.
Notes related to The soundness of bugs is what matters (position statement)
Papers related to The soundness of bugs is what matters (position statement)
- Incorrectness logic [ohearn:popl:2019]
- Soundness and its role in bug detection systems [xie:bugs:2005]