ABSTRACT. 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). In summary, JBMC processes Java bytecode together with a model of the standard Java libraries, with the goal of checking a set of desired properties. Experimental results show that JBMC can correctly verify a set of Java benchmarks extracted from the literature and it also performs competitively with JayHorn and JPF, which are state-of-art Java veriers based on constrained Horn clauses and path-based symbolic execution, respectively.