3 ms·

> You test all possible values Which is not feasible if there are, say 2^128 or more possible values. CBMC is a model checker, which is very useful for many pr

> You test all possible values Which is not feasible if there are, say 2^128 or more possible values. CBMC is a model checker, which is very useful for many problems that can be brute-forced but not the same thing as the correct-by-construction approach of Frama-C style formal methods, which deductively verifies that code works on all possible cases, even all conceivable edge cases, without having to exhaustively test all cases.

rurban 5y ago
CBMC does formal verification on symbolic values and its ranges, just as Frama-C. Just in a well-known language, C. There is no brute force search. If so it would be impractical. The industry is using CBMC, not Frama-C.
- dandotway 5y ago
  I just went through the CBMC tutorial[1] to make sure I'm not crazy. Yes, CBMC is a bounded model checker, as I thought. CBMC can also be used for programs with unbounded loops. In this case, CBMC is used for bug hunting only; CBMC does not attempt to find all bugs. Frama-C is about eliminating ALL bugs, you are allowed to prove your "unbounded" loop algorithm actually terminates, and terminates with the correct solution, if you are willing to learn to use the manual proof assistant. CBMC can check for an extremely important class of errors, but it doesn't let you prove, say, your traveling salesman solver always returns a shortest trip T through the graph G, or that the graph coloring register allocator for your C compiler always correctly colors the graph, something that is actually done for the CompCert formally verified C compiler (using the Coq/Gallina proof assistant, which can be used with Frama-C). However, having now gone through the CBMC manual, it appears to be much faster and easier to use for my own limited purposes than Frama-C. I don't need a sledgehammer to swat flies. I also like that the installation procedure on my machine was simply, $ sudo apt install cbmc So I plan to give cprover a shot now, thanks for the heads up. : ) [1] http://www.cprover.org/cprover-manual/cbmc/tutorial/ http://www.cprover.org/cprover-manual/cbmc/tutorial/

rurban 5y ago

CBMC does formal verification on symbolic values and its ranges, just as Frama-C. Just in a well-known language, C. There is no brute force search. If so it would be impractical. The industry is using CBMC, not Frama-C.

dandotway 5y ago
I just went through the CBMC tutorial[1] to make sure I'm not crazy. Yes, CBMC is a bounded model checker, as I thought. CBMC can also be used for programs with unbounded loops. In this case, CBMC is used for bug hunting only; CBMC does not attempt to find all bugs. Frama-C is about eliminating ALL bugs, you are allowed to prove your "unbounded" loop algorithm actually terminates, and terminates with the correct solution, if you are willing to learn to use the manual proof assistant. CBMC can check for an extremely important class of errors, but it doesn't let you prove, say, your traveling salesman solver always returns a shortest trip T through the graph G, or that the graph coloring register allocator for your C compiler always correctly colors the graph, something that is actually done for the CompCert formally verified C compiler (using the Coq/Gallina proof assistant, which can be used with Frama-C). However, having now gone through the CBMC manual, it appears to be much faster and easier to use for my own limited purposes than Frama-C. I don't need a sledgehammer to swat flies. I also like that the installation procedure on my machine was simply, $ sudo apt install cbmc So I plan to give cprover a shot now, thanks for the heads up. : ) [1] http://www.cprover.org/cprover-manual/cbmc/tutorial/ http://www.cprover.org/cprover-manual/cbmc/tutorial/