Open source projects

Difflblue products and labs initiatives are built on open source projects and cutting edge research by members of our team and their collaborators. We invite you to explore, contribute and get in touch.


CBMC: Bounded Model Checker for C and C++ programs

CBMC verifies array bounds (buffer overflows), pointer safety, ex­cep­tions and user-specified as­ser­tions. CBMC comes with a built-in solver for bit-vector formulas that is based on MiniSat. As an alternative, CBMC has featured support for external SMT solvers since version 3.3. The solvers we recommend are (in no particular order) Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be installed separately and have different licensing conditions. Interested developers and researchers from the community please contact us to get in touch, see example applications or engage with the community on Google and GitHub below.


JBMC: Bounded Model Checker for Java programs

JBMC checks runtime exceptions and user-defined assertions. The verification is performed by unwinding the loops in the program and passing the resulting formula to a decision procedure. Interested developers and researchers from the community please contact us to get in touch, see example applications or engage with the community on Google and GitHub below.


Fastsynth: Code Refactoring and Code Repair

Fastsynth automatically generates programs which satisfy a specification expressed as user-defined assertions. It uses JBMC under the hood to decide whether the generated program satisfies the specification.

Interested developers and researchers from the community please contact us here to get access to a compiled version or more information.


Synth4j: Code Refactoring and Code Repair

Synth4j is a Java API for JBMC and fastsynth. It simplifies inserting assertions into Java user programs to verify certain properties about the programs. The same mechanism is used to express specifications to generate programs that behave in a desired way.

The framework is used by Diffblue to express refactoring and program repair features, automatically improving developer code or fixing bugs. The API is made available to customers to express their own automated analyses and transformations of their Java code.

Interested developers and researchers from the community please contact us here to get access to source code or more information.


CBMC and JBMC include software developed by Daniel Kroening, Edmund Clarke, Computer Science Department, University of Oxford, Computer Science Department, Carnegie Mellon University