I have been using CBMC to formally verify C for six, make that seven years now (edit: time flies). The latest release is actually pretty good.
The secret to model checking is to understand that you're building and verifying a specification in code. It works best if specifications are built function by function. For each function, I'll build "shadow functions" that simplify any functions it calls with a range of potential non-deterministic behavior that matches that function's contract. In this way, formal specifications can be built from the ground up by first verifying a lower-level function and then replacing it with a shadow function that mimics its behavior in a non-deterministic but SMT solver friendly way.
There are things that model checking doesn't do well. Anything with recursion or looping that can't be easily broken down will not perform well with a model checker. While algorithms like balanced binary trees or sorting can be broken down in a way that can be model checked, other algorithms may require the sort of induction one gets with constructive proofs to sufficiently verify. There is an art to this which will lead to style changes in C and a slightly different way of building up functions from pieces that can be trivially model checked. Honestly, that's not a bad thing.
For the parts that can't be easily model checked, I'm working on a C parser library that can be formally verified, which will import C directly into Coq or Lean. I consider that the "last mile" before formal methods in firmware and system software is to the point that it's generally available.
> [...] other algorithms may require the sort of induction one gets with constructive proofs to sufficiently verify. There is an art to this which will lead to style changes in C and a slightly different way of building up functions from pieces that can be trivially model checked.
Is there a book or article that talks more about this? I.e. how to write code in a way that is more amenable to model-checking (bounded or otherwise)?
If the tool exists and has minimal overhead, I don't think it is a matter of permission but a matter of necessity. CBMC adds about 30% overhead over just unit testing, in my experience. It does require a different idiomatic programming style to use correctly, and there is a learning curve. Some intuition is required to learn how to use the tool effectively and efficiently, but this can be taught.
For system programming or firmware, it's incredibly useful. I've used this tool in conjunction with threat modeling and attack surface minimization to significantly improve the safety and security of software written in C. At this point, I would not consider working on any C project that did not make use of this tool.
Not fun, a serious tool, and extremely easy to use, unlike other formal methods. It works with your source code, not on some rewritten abstraction of it.
Embedded, automotive, space use it regularly.
I've setup cbmc and goto-analyzer for string searching algos here https://github.com/rurban/smart and really found some bugs in old published algos.
The secret to model checking is to understand that you're building and verifying a specification in code. It works best if specifications are built function by function. For each function, I'll build "shadow functions" that simplify any functions it calls with a range of potential non-deterministic behavior that matches that function's contract. In this way, formal specifications can be built from the ground up by first verifying a lower-level function and then replacing it with a shadow function that mimics its behavior in a non-deterministic but SMT solver friendly way.
There are things that model checking doesn't do well. Anything with recursion or looping that can't be easily broken down will not perform well with a model checker. While algorithms like balanced binary trees or sorting can be broken down in a way that can be model checked, other algorithms may require the sort of induction one gets with constructive proofs to sufficiently verify. There is an art to this which will lead to style changes in C and a slightly different way of building up functions from pieces that can be trivially model checked. Honestly, that's not a bad thing.
For the parts that can't be easily model checked, I'm working on a C parser library that can be formally verified, which will import C directly into Coq or Lean. I consider that the "last mile" before formal methods in firmware and system software is to the point that it's generally available.