book chapter · Lecture notes in computer science · 2018

JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode

Lucas C. Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, Marek Trtík

Cited by 68Open access

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.

Cite this paper

APA 7

Cordeiro, L. C., Kesseli, P., Kroening, D., Schrammel, P., & Trtík, M. (2018). JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. Lecture notes in computer science, 183–190. https://doi.org/10.1007/978-3-319-96145-3_10

MLA 9

Cordeiro, Lucas C., et al. “JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode.” Lecture notes in computer science, 2018, pp. 183–90, https://doi.org/10.1007/978-3-319-96145-3_10.

Chicago

Cordeiro, Lucas C., Pascal Kesseli, Daniel Kroening, Peter Schrammel, and Marek Trtík. 2018. “JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode.” Lecture notes in computer science: 183–90. https://doi.org/10.1007/978-3-319-96145-3_10.

Harvard

Cordeiro, L.C. et al. (2018) ‘JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode’, Lecture notes in computer science, pp. 183–190. Available at: https://doi.org/10.1007/978-3-319-96145-3_10.

BibTeX

@incollection{cordeiro2018jbmc,
  title = {{JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode}},
  author = {Cordeiro, Lucas C. and Kesseli, Pascal and Kroening, Daniel and Schrammel, Peter and Trtík, Marek},
  booktitle = {Lecture notes in computer science},
  pages = {183--190},
  year = {2018},
  doi = {10.1007/978-3-319-96145-3_10}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.