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!
I just released bmc4j, a tool that lets you write proofs about Java/Kotlin code as ordinary JUnit 5 tests.
For example:
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!