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
CITATION STYLE
Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., & Trtik, M. (2018). JBMC: A bounded model checking tool for verifying java bytecode. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10981 LNCS, pp. 183–190). Springer Verlag. https://doi.org/10.1007/978-3-319-96145-3_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
