Introduction

What is bmc4j?

bmc4j is a bounded model checker software verification tool built on top of JBMC. You write your proofs as easy to digest tests and run them like any other test.

import org.bmc4j.Bmc.*
import org.bmc4j.BmcProof
import org.bmc4j.kotlin.assumeValid

@JvmInline
value class Score(val value: Int) { init { require(value in 1..100) } }

class GradeBandProofs {

    @BmcProof
    fun `Score invariant holds`() {
        // run the constructor over ALL ints, the require causes the domain of anyInt() to fold to 1..100
        val s = assumeValid { Score(anyInt()) }
        // proves that the s.value never exceeds the range defined in the require in init
        check(s.value in 1..100)
    }

    @BmcProof
    fun `gradeBand never throws for any Score`() {
        // require(...) folded into the domain automatically by assumeValid
        val score = assumeValid { Score(anyInt()) }

        // function under test - refutes if any exception, assertion or error happens for the folded domain
        gradeBand(score.value)
    }
}

What is Bounded Model Checking?

Instead of running your code on some inputs, BMC translates your built code into a logic formula, which is then solved by a SAT solver. If the SAT solver comes back as unsatisfiable (there’s no assignment of literals that can satisfy the logic formula), your proof is sound. On the other hand, if it comes back satisfying the formula, that’s a counter-example - it’s mapped back to the input and presented to you.

Limitations, Trade-offs, When to use it

See https://github.com/bmc4j/bmc4j/blob/main/README.md

Key Concepts

3 Way Verification

In bmc4j our most important goal is soundness. Proofs written will always return one of:

• Verified - the proof holds and your code is sound sequentially.
• Refuted - An input that breaks the asserted properties - a counter-example.
• Unknown - engine crashed, timeout, unwinding not sufficient.

Unwinding

Unwinding means to “un-wind” the iterations of a loop.

Take the following loop:

while (true) {
  doThing()
}

How do you turn this into a proof? You can’t! Instead you bound the model to a fixed set of iterations to do a bounded proof, so an unwinding of 4 would collapse into:

  doThing();
  doThing();
  doThing();
  doThing();

This raises one big concern: how can I take this proof as a meaningful verdict if my code does more iterations?

In bmc4j our answer is to return Unknown - if execution could run past the bound, we won’t claim Verified on a loop we couldn’t fully explore.

By default you don’t pick the bound at all: bmc4j finds one for you, trying increasing bounds until the loops are fully covered, then verifying. A loop it can’t cover within the cap (like the while (true) above) comes back Unknown — never a false Verified. It reports the bound it settled on, so you can pin @BmcProof(unwind = N) to lock it in — handy to skip the search, or to push a deep loop past the default cap.

Model

A model is a drop-in replacement for a class/method that replaces the real class to help keep proofs small. An example of this is our SortWitness, instead of having a full JDK sort algorithm in your proof, we take the JDK sort algorithms as sound and return you a “witness” model that just asserts the properties.

Havoc

Havocing means replacing a method with a non-deterministic result. This is what happens to classes outside the models or your code.

Why? bounded model checking proofs can be slow, turning the entire class-code verbatim into a proof would be next to impossible to solve, and arguably not useful.

Take an InputStream for example - you know it’s going to return a non-deterministic set of data, so its bytecode is not relevant to the proof, it’s replaced with a stub that returns the non-deterministic value.