First-time users of CBMC or Kani customers reach the limits of the tool (space-out or time-out) and are discouraged from using the tool. Existing users that try to extend formal verification to larger functions, or towards more functional properties are also likely reach the limits of the tool. Providing better scalability out of the box will help widen the adoption of FV for new users (eg: AL2, firecrab, etc. ) and extend the guarantees offered to existing users (FireTV, s2n-tls, aws-c-commons, etc). Our goal is to bring algorithmic improvements to the core algorithms in use today, that translate to a significant improvement for our users, as measured by the number of new problems solved on the benchmark suite, as well as the number of benchmarks amenable to unbounded verification.
CBMC currently uses a bit-precise forward symbolic execution algorithm for GOTO programs that reduces verification to SAT with a very detailed memory model. There are many complementary model checking algorithms for GOTO-like languages, which could complement the default algorithm of CBMC: backwards symbolic simulation with loop folding, predicate abstraction, CEGAR algorithms, PRD algorithms, etc. to name a few. Our goal is to bring at least one of these alternative techniques to GOTOz programs, in order to be able to solve at least 50% of customer benchmarks that are identified as unsolvable today in our performance regression suite.
In addition, the ability to perform unbounded verification is currently very limited (in the case of CBMC) or non-existent (in the case of Kani). We would like to add support for unbounded verification of array-manipulating programs in both CBMC and Kani through enabling an unbounded verification engine through one of the following means:
- Integrating a Constrained Horn Clauses (CHC) engine in CBMC
- Integrating an existing tool that supports unbounded verification (e.g. Creusot (https://github.com/xldenis/creusot) or Gillian (https://github.com/GillianPlatform/Gillian))
- Completing the support for function/loop contracts and hooking up this support in Kani
Issues
- model-checking/kani#2015 · opened
on Dec 16, 2022 · Extend the Capabilities of GOTO Verification Engines - model-checking/kani#2302 · opened
on Mar 17, 2023 · Extend the Capabilities of GOTO Verification Engines - model-checking/kani#2801 · opened
on Oct 2, 2023 · Extend the Capabilities of GOTO Verification Engines - model-checking/kani#4667 · opened
on Jul 22, 2026 · Extend the Capabilities of GOTO Verification Engines - model-checking/kani#2001 · opened
on Dec 14, 2022 · Extend the Capabilities of GOTO Verification Engines - model-checking/kani#4965 · opened
on Oct 4, 2026 · Extend the Capabilities of GOTO Verification Engines