JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)

Lucas Cordeiro, Daniel Kroening, Peter Schrammel

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


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.
Original languageEnglish
Title of host publicationInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems
Publication statusPublished - 4 Apr 2019


Dive into the research topics of 'JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)'. Together they form a unique fingerprint.

Cite this