4 ms·

First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major str

by pron 7y ago

First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major strength, though. Second, engineers build systems, and they care about the correctness of their system. This is something that cannot possibly be proven because a system is a physical object, and at best, what you can get are probabilistic guarantees (e.g. the CPU only performs the commands it is given with some probability). So what engineers want (as opposed to mathematicians or computer scientists publishing an algorithm) is a technique that most cheaply brings their system to the required correctness probability. Whether this means proving the algorithm correct or finding as many bugs as possible is completely irrelevant. So far, automated techniques like the ones I mentioned do a better job at that, and that is why they're currently considered more promising.

zozbot234 7y ago
> First, model checking is a proof technique It is a proof technique if you're exhaustively checking a finite model, but the usual meaning of "model checking" is not restricted to that case. You may be right that just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. Probably for "global", cross-cutting properties where formal proof might be expected to be difficult.
- pron 7y ago
  > but the usual meaning of "model checking" is not restricted to that case It is. That's the definition of the term "model checking" ("model" means a satisfying assignment for a logic formula). Some model checkers (like CEGAR) also exhaustively check infinite-state specifications (although, obviously, not in every case; BTW, that model checkers are exhaustive, meaning sound, does not mean that they operate by brute-force -- they do not). You are, however, correct that sometimes we model check only a finite instance of a program/spec with infinite states, but in this case it is that restricted spec that is model-checked. That is one of the many ways in which model checking is more flexible than deductive proofs. > just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. It would, does, and must suffice for all use cases, and besides, there is no other alternative. > Probably for "global", cross-cutting properties where formal proof might be expected to be difficult. No real system can be guaranteed to be correct. It is a physical impossibility. There is simply no such thing as a system that is "proven correct" in formal methods; the best you can hope for is an algorithm that is proven correct or a system that is correct with probability. Even exhaustive (i.e. sound) techniques like formal deductive proofs and model checking only guarantee the correctness of a system with probability. An algorithm that is proven to give the right answer is only a probabilistic guarantee that the system will (because the guarantee that the computer will execute the commands given to it correctly is only probabilistic). Mathematicians and algorithm authors can prove theorems; engineers only need, and can only ever hope for, probabilities. This is why while there may be some overlap in the computer-assisted techniques offered to mathematicians and algorithms writers, the study of software verification is concerned with a different problem.

by pron 7y ago

zozbot234 7y ago

> First, model checking is a proof technique It is a proof technique if you're exhaustively checking a finite model, but the usual meaning of "model checking" is not restricted to that case. You may be right that just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. Probably for "global", cross-cutting properties where formal proof might be expected to be difficult.

pron 7y ago
> but the usual meaning of "model checking" is not restricted to that case It is. That's the definition of the term "model checking" ("model" means a satisfying assignment for a logic formula). Some model checkers (like CEGAR) also exhaustively check infinite-state specifications (although, obviously, not in every case; BTW, that model checkers are exhaustive, meaning sound, does not mean that they operate by brute-force -- they do not). You are, however, correct that sometimes we model check only a finite instance of a program/spec with infinite states, but in this case it is that restricted spec that is model-checked. That is one of the many ways in which model checking is more flexible than deductive proofs. > just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. It would, does, and must suffice for all use cases, and besides, there is no other alternative. > Probably for "global", cross-cutting properties where formal proof might be expected to be difficult. No real system can be guaranteed to be correct. It is a physical impossibility. There is simply no such thing as a system that is "proven correct" in formal methods; the best you can hope for is an algorithm that is proven correct or a system that is correct with probability. Even exhaustive (i.e. sound) techniques like formal deductive proofs and model checking only guarantee the correctness of a system with probability. An algorithm that is proven to give the right answer is only a probabilistic guarantee that the system will (because the guarantee that the computer will execute the commands given to it correctly is only probabilistic). Mathematicians and algorithm authors can prove theorems; engineers only need, and can only ever hope for, probabilities. This is why while there may be some overlap in the computer-assisted techniques offered to mathematicians and algorithms writers, the study of software verification is concerned with a different problem.