other · Zenodo (CERN European Organization for Nuclear Research) · 2025

JBMC: Bounded Model Checking for Java Bytecode

Schrammel, Peter

Cited by 0Open access

Abstract

JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.

Cite this paper

APA 7

Schrammel, P. (2025). JBMC: Bounded Model Checking for Java Bytecode. Zenodo (CERN European Organization for Nuclear Research). https://doi.org/10.5281/zenodo.17688623

MLA 9

Schrammel, Peter. “JBMC: Bounded Model Checking for Java Bytecode.” Zenodo (CERN European Organization for Nuclear Research), 2025, https://doi.org/10.5281/zenodo.17688623.

Chicago

Schrammel, Peter. 2025. “JBMC: Bounded Model Checking for Java Bytecode.” Zenodo (CERN European Organization for Nuclear Research). https://doi.org/10.5281/zenodo.17688623.

Harvard

Schrammel, P. (2025) ‘JBMC: Bounded Model Checking for Java Bytecode’, Zenodo (CERN European Organization for Nuclear Research). Available at: https://doi.org/10.5281/zenodo.17688623.

BibTeX

@misc{schrammel2025jbmc,
  title = {{JBMC: Bounded Model Checking for Java Bytecode}},
  author = {Schrammel, Peter},
  journal = {Zenodo (CERN European Organization for Nuclear Research)},
  year = {2025},
  doi = {10.5281/zenodo.17688623}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.