[trustable-software] Model Checkers

Maciej Wolny maciej.wolny at codethink.co.uk
Fri Sep 21 15:45:27 BST 2018


On 21/09/2018 14:10, Ben Brewer wrote:
> The website for MOPS states that it's not a checker itself, but a framework for adding your own checks, so I highly suspect that the reason it could be run over an entire distro is that they ran a very minimal set of checks; the paper also suggests this as they only found 138 bugs in the distribution, while I believe it's reasonable to assume that there are a lot more than that.

If you're coming from a perspective of finding all bugs, you're going to be disappointed forever. Not only that, this perspective is dangerous, because any procedure/tool that you believe to be satisfying this requirement will give you a false sense of security. 138 bugs is in and of itself neither a big or small. That being said, personally, I would be proud of this result, and would consider it an important contribution to the bug-finding effort.



More information about the trustable-software mailing list