Is Code Verification Finally Good Enough?

Jonathan asks: "As someone who has been following the development of software verification technology, a recent trend has intrigued me. It seems that the formal method people have finally come down off their high horse and are offering code verification as just another tool. This approach shows up in recent Java and C# based code verification tools that aren't aimed at 'proving correctness' so much as finding potential errors. Now it seems that such an approach is beginning to find its way into XP methods[pdf] as another verification tool to supplement unit tests. Given the current speed and effectiveness of tools like the Spec# verifier, is code verification via automated theorem proving finally going to make its way into the mainstream?"

Comments

Re:Excuse me, did any of you graduate yet?

[Fahrenheit 450]

Well, it's quite possible to do things like restrict the problem to a decidable subset of the original problem and only let your solution work on those subsets. Or you can work on problems that are undecidable in general, but in most typical cases are not only decidable, but efficiently solvable. For example, most type systems work in one of these two ways.

You see, you should have learned before you graduated that just because a problem is hard (or impossible) in general, that doesn't mean the average case is hard at all.

Re:Not possible

[Coryoth]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself? In other words, if you can write a description of what the program should do that is more accurate than the program, then that description should replace the source code.

It is often easier to describe what a program has to do than it is to describe exactly how to do it. I can describe what a square root finding algorithm has to do: given x it has to find y such that y*y =x; without coming close to writing something that actaully finds the square root. All the prover then has to do is ensure that the code instructions really do produce a result that satisfies the stated constraint - which is potentially entirely possible. Writing contracts for code can be as easy (or easier) than writing unit tests for code. If you write a contract instead of a unit test then that potentially gives the prover all it needs to verify that the code will work for all possible test cases instead of your predefined unit test cases. If the prover can't manage that then just feed in some test data and if the contract fails you've found an error (that is, at worst you've got a unit test already). Working this way can be remarkably efficient at weeding out errors - you verify code when it works, and essentially do unit testing for the code that can't be verified. Perhaps if you actually tried it you'd see.

Re:a chain of crutches

[neutralstone]

Regardless of the poor decisions of some recruiters, I've found this to be true: the most competent and disciplined engineers tend to use as many checking techniques as possible (e.g., regression tests, unit tests, multiple static analysis tools, etc.). They use these techniques not as a substitute for a disciplined approach to design or to implementation (that would be foolish), but as a sanity check on a finished product. They use multiple checking techniques because they know they're human, and humans -- even the most skilled, most experienced, most disciplined ones -- make mistakes, and they want to do everything they reasonably can to catch mistakes before a product ships.

So to that end, model checkers (and other forms of checking) are Good Things(TM). The possibility that some will misconstrue checking facilities as a substitute for competent and disciplined engineers is a separate issue, and it's not the fault of the checking scheme. The *organizational* problem of poor recruiting cannot be solved by getting rid of model-checking systems, and if your recruiters think that talent can be replaced by a "verification" system, you've got bigger problems than merely the shoddy designs that will come down the pike.

(Please note that I prefer to use the term "check" rather than "verify", because the latter term, when used to describe a program, too easily connotes the notion that a "verified" program is free of any bugs (which is, needless to say, always a dubious claim). "Check" on the other had usually connotes the idea that there is a specific bug (or set of specific bugs) that is tested for. Of course, TFA mentions they don't want to imply that (verification == no bugs). But IMHO too many people make that mistake.)