Treffer: JBMC: Bounded Model Checking for Java Bytecode
Title:
JBMC: Bounded Model Checking for Java Bytecode
Authors:
Publisher Information:
Zenodo
Publication Year:
2024
Collection:
Zenodo
Document Type:
E-Ressource
software
Language:
English
Relation:
https://zenodo.org/records/13975618; oai:zenodo.org:13975618; https://doi.org/10.5281/zenodo.13975618
DOI:
10.5281/zenodo.13975618
Rights:
BSD 3-Clause "New" or "Revised" License ; bsd-3-clause ; https://opensource.org/licenses/BSD-3-Clause ; BSD 4-Clause "Original" or "Old" License ; GNU General Public License v2.0 only
Accession Number:
edsbas.D5882DE2
Database:
BASE
Weitere Informationen
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. ; Licenses: JBMC: BSD 4-Clause java-cprover-api.jar: BSD 3-Clause core-models.jar: GPL2 with classpath exception