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.


Have Diffblue Cover test your public GitHub Java repository for free

Diffblue has a history of involvement in the Open Source community and is committed to providing unit tests to public repositories without obligation. We’ve also found this to be an effective way to continually test our product against diverse code bases. Diffblue Cover is a program that writes unit tests for Java code bases. The obvious benefit to repo owners is free tests(!) which saves time for contributors to spend on developing code. Diffblue gains from any feedback received to help us continue to improve the tool.

If you’d like to have Diffblue Cover test your public GitHub Java repository for free, please provide the GitHub URL and a contact email address below.

http://

You can also browse our recently merged PR requests, FAQs and ask questions on our Open Source FAQ page.

We will process your personal data in accordance with our Privacy Notice.


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