Tools that use sound, i.e. over-approximating a rigorous model, formal methods approach to static analysis (e.g., using static program assertions). Sound methods contain no false negatives for bug-free programs, at least with regards to the idealized mathematical model they are based on (there is no "unconditional" soundness). Note that there is no guarantee they will report all bugs for buggy programs, they will report at least one.
Astrée– finds all potential runtime errors by abstract interpretation, can prove the absence of runtime errors and can prove functional assertions; tailored towards safety-critical C code (e.g. avionics).
CodePeer– Statically determines and documents pre- and post-conditions for Ada subprograms; statically checks preconditions at all call sites.
Frama-C– An open-source analysis framework for C, based on the ANSI/ISO C Specification Language (ACSL). Its main techniques include abstract interpretation, deductive verification and runtime monitoring.
KeY– analysis platform for Java based on theorem proving with specifications in the Java Modeling Language; can generate test cases as counterexamples; stand-alone GUI or Eclipse integration
MALPAS– A formal methods tool that uses directed graphs and regular algebra to prove that software under analysis correctly meets its mathematical specification.
Polyspace– Uses abstract interpretation, a formal methods based technique,[17] to detect and prove the absence of certain run time errors in source code for C/C++, and Ada
