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

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). 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
DOIs
Publication statusPublished - 18 Jul 2018

Keywords

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

Fingerprint

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

Cite this