JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
- Submitting institution
-
The University of Manchester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 103062768
- Type
- G - Software
- Name of software house
- Springer Nature
- Month
- July
- Year
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
A - Computer Science
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- JBMC is the first software to achieve bit-level verification of Java code.
JBMC is the primary technology behind a commercial tool called Diffblue Cover, marketed by Diffblue Ltd. JBMC enables Diffblue Cover to automatically generate unit tests, thereby improving developers' productivity, and assuring coverage of the program state-space. It also enhances existing regression (test) suites, allowing software developers to understand the impact of changes and make more informed development decisions. DiffBlue Cover is heavily used by software engineers within GoldmanSachs and Amazon Web Services.
JBMC was published as a tool paper at CAV 2018 and received an artefact evaluation badge, i.e. the work was independently confirmed as fully reproducible.
In the international competition on software verification (2019) JBMC won first place in the overall ranking for the Java track.
JBMC stimulated follow-on work which contributed to community standards, used to generate benchmarks for checking the completeness/soundness of software verification tools. At the end of the REF period, the GitHub repository has 298 stars and 163 forks.
For full details, see accompanying PDF file.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
