3 ms·

In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and

In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and others. I consider bounded model checking to be "formal methods lite". It provides most of the benefits at a lower cost of entry than using a proof assistant or building constructive proofs. Really, there's little added overhead. Perhaps 30% to 40% more time to build out the function contracts and model checking. Given that this overhead more or less prevents errors that would likely be introduced without it, I think it's a reasonable investment. TLA+ is certainly related, since it uses an SMT solver at its base. I see it as useful for designing algorithms and protocols. A tool like CBMC or Kani provides similar guarantees at the source code level. It's not perfect, as currently CProver does not have direct threading support, but with a reasonable application of method shadowing and function contracts, even things like threading can be anticipated. Using a bounded model checker effectively means changing the design of software to work best with it. This is little different than using concepts like TDD or continuous integration.

vlovich123 2y ago
In my experience traditional property checks are pretty difficult to write already (30-40%). I get the sense that a bounded model check would be even more expensive than that, probably into the 2-3x range if not more. I’m talking about meaningfully complex logic, not very simple things.
- rtpg 2y ago
  It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy to write, when your property aligns well with property checking models! But then time-based stuff like TLA+ ends up working way better, sometimes. There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.
- nanolith 2y ago
  You can write these checks as assertions in your regular source language. It's no more difficult than writing runtime parameter checks, really. There are some complexities, to be fair, but these are mostly around the performance of the model checker. Some things are easy to check, and other things, like loops and recursion, are harder to check. However, this is a matter of optimization, and with practice, this becomes quite easy to deal with.
  - vlovich123 2y ago
    As I said I use property checks as much as possible, but they’re still cumbersome and the complexity and difficulty scale non-linearly with the complexity of the interface; some properties are easy to write whereas others are so difficult I can’t imagine how to write a generic property for all situation vs resorting to boundary conditions I think of. The challenges with the model checker is that there’s all sorts of constructs it can’t test. For example, Kani can’t handle await expressions which is a huge obstacle for any async Rust code.
    - nanolith 2y ago
      Threading and async are an issue with the current CProver core. But, much of that can be simulated by writing helper functions that get shadowed during the model checking. It's simply not possible to make a bounded model checker work on arbitrary code, so instead, the code should be factored to work within the constraints of the model checker. The result is safer code, even if the style is different.
      - vlovich123 2y ago
        I never said threading. I use a single-threaded runtime. But the lack of any async support even though it’s basically syntactic sugar at that point makes it a non-starter. There’s some amount of “make your code testable” that’s valid, but completely rewrite how your application is written and thus you can’t use the frameworks you need to is a bit much. At some point the testing framework has to also meet you where you are.
siscia 2y ago
In Java it would be something like JBMC?
- nanolith 2y ago
  Yep. JBMC is part of the CProver / CBMC family.

vlovich123 2y ago

In my experience traditional property checks are pretty difficult to write already (30-40%). I get the sense that a bounded model check would be even more expensive than that, probably into the 2-3x range if not more. I’m talking about meaningfully complex logic, not very simple things.

rtpg 2y ago
It would be interesting to have a workbook of what people consider valuable examples of issues we are trying to solve. Like property checks are sometimes easy to write, when your property aligns well with property checking models! But then time-based stuff like TLA+ ends up working way better, sometimes. There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.
nanolith 2y ago
You can write these checks as assertions in your regular source language. It's no more difficult than writing runtime parameter checks, really. There are some complexities, to be fair, but these are mostly around the performance of the model checker. Some things are easy to check, and other things, like loops and recursion, are harder to check. However, this is a matter of optimization, and with practice, this becomes quite easy to deal with.
- vlovich123 2y ago
  As I said I use property checks as much as possible, but they’re still cumbersome and the complexity and difficulty scale non-linearly with the complexity of the interface; some properties are easy to write whereas others are so difficult I can’t imagine how to write a generic property for all situation vs resorting to boundary conditions I think of. The challenges with the model checker is that there’s all sorts of constructs it can’t test. For example, Kani can’t handle await expressions which is a huge obstacle for any async Rust code.
  - nanolith 2y ago
    Threading and async are an issue with the current CProver core. But, much of that can be simulated by writing helper functions that get shadowed during the model checking. It's simply not possible to make a bounded model checker work on arbitrary code, so instead, the code should be factored to work within the constraints of the model checker. The result is safer code, even if the style is different.
    - vlovich123 2y ago
      I never said threading. I use a single-threaded runtime. But the lack of any async support even though it’s basically syntactic sugar at that point makes it a non-starter. There’s some amount of “make your code testable” that’s valid, but completely rewrite how your application is written and thus you can’t use the frameworks you need to is a bit much. At some point the testing framework has to also meet you where you are.

siscia 2y ago

In Java it would be something like JBMC?

nanolith 2y ago
Yep. JBMC is part of the CProver / CBMC family.