Hacker News Reader

Comment by rurban | Hacker News Reader

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.

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/

Reply on news.ycombinator.com