A tool for advanced static error detection using program verification technology with automatic theorem prover. Programmer specifies pre/post-conditions and invariants in comments of the Java program. They are similar to asserts, with the difference that the source is checked for validity only statically.
-- NikolaToshev
Is this synonymous with as StaticAnalysis?