Two others worth checking out that focus on soundness with low to no false positives are RV-Match and TrustinSoft Analyzer: https://runtimeverification.com/mat

Two others worth checking out that focus on soundness with low to no false positives are RV-Match and TrustinSoft Analyzer: https://runtimeverification.com/match/ https://runtimeverification.com/match/ https://trust-in-soft.com/products/ https://trust-in-soft.com/products/ The RTV people are the one's behind K framework and an executable semantics for C with a GCC-like interface: http://www.kframework.org/index.php/Main_Page http://www.kframework.org/index.php/Main_Page https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics That RV-Match builds on an open framework, does well on benchmarks (yeah skepticism here), and has little to no noise (most important) is what I like most about it. I say most important since digging through false positives makes developers not want to use a tool. I haven't tried either product myself, though. Here's a list of open tools that did well in small-scale experiments with and without false positives: https://klee.github.io https://klee.github.io http://www.cprover.org/cbmc/ http://www.cprover.org/cbmc/ https://cseweb.ucsd.edu/~rjhala/blast.html https://cseweb.ucsd.edu/~rjhala/blast.html http://www.splint.org http://www.splint.org http://spinroot.com/uno/ http://spinroot.com/uno/ http://cppcheck.sourceforge.net/#features http://cppcheck.sourceforge.net/#features https://en.wikipedia.org/wiki/Sparse https://en.wikipedia.org/wiki/Sparse https://cpachecker.sosy-lab.org https://cpachecker.sosy-lab.org