Extended static checking is a powerful program analysis technique. It translates into a logical formula the hypothesis that a given program has some particular desirable properties. The logical formula, calleda verification condition, is then checked with an automatic theorem prover. The extended static checking technique has been built into a couple of program checkers. This paper discusses other possible applications of the technique to the problem of producing quality software more quickly.
['K. Rustan M. Leino']
Applications of Extended Static Checking