JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode

Lucas Cordeiro, Pascal Kesseli, D. Kroening, Peter Schrammel, Marek Trtik

Research output: Non-textual formSoftware


We present a bounded model checking tool for verifying Java bytecode, which is built on top of the CPROVER framework, named Java Bounded Model Checker (JBMC). JBMC processes Java bytecode together with a model of the standard Java libraries and checks a set of desired properties. Experimental results show that JBMC can correctly verify a set of Java benchmarks from the literature and that it is competitive with two state-of-the-art Java verifiers.
Original languageEnglish
PublisherSpringer Nature
Publication statusPublished - 18 Jul 2018


  • Software Verification
  • Bounded Model Checking
  • Formal Methods
  • Java


Dive into the research topics of 'JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode'. Together they form a unique fingerprint.

Cite this