Grover_c13

11 ms·

1. 1.▲
   by Grover_c13 3mo ago

   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 wor
2. 2.▲
   Bmc4j – Prove your Java/Kotlin code correct from jUnit style tests(github.com)

   3 points by Grover_c13 4mo ago|4 comments
3. 3.▲
   by Grover_c13 4mo ago

   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(),