Bmc4j – Prove your Java/Kotlin code correct from jUnit style tests(github.com)

3 pointsby Grover_c13mese scorso4 comments

Bmc4j – Prove your Java/Kotlin code correct from jUnit style tests

https://github.com/bmc4j/bmc4j

4 comments

Hi HN!

I just released bmc4j, a tool that lets you write proofs about Java/Kotlin code as ordinary JUnit 5 tests.

For example:

  @BmcProof
  void clamp_result_is_always_within_bounds() {
      int x = Bmc.anyInt(), lo = Bmc.anyInt(), hi = Bmc.anyInt();
      Bmc.assume(lo <= hi);
      int r = Example.clamp(x, lo, hi);
      Bmc.check(r >= lo && r <= hi);
  }

then you can run it like any other test, you will get a result indicating its verified, refuted (and you get the input and replay test, or unknown (reached a timeout etc).

The repo is full of a bunch of examples and docs on how it works, take a look and feel free to ask any questions!

emmemese scorso

It seems very interesting, thank you. What's the relationship with the original jbmc project?

Grover_c13mese scorso

We use JBMC as the engine to do the verification (unmodified). bmc4j is independent of the group, we just use the tooling (similar to kani using cbmc).

if you used you it may be aware of the gaps when it comes to java, so bmc4j does leg work to fill it in (lots of JDK modelling, kotlin intrinsics, some byte-code transformation to fill in soundness holes) while trying making the developer experience not so painful.

emmemese scorso

Yes, great work, thank you. I tried it a bit, and the experience is much more pleasant than using jbmc directly.