JBMC: a bounded model checking tool for verifying java bytecode

Cordeiro, Lucas, Kesseli, Pascal, Kroening, Daniel, Schrammel, Peter and Trtik, Marek (2018) JBMC: a bounded model checking tool for verifying java bytecode. CAV 2018- 30th International Conference on Computer Aided Verification, Oxford, UK, July 14-17, 2018. Published in: CAV 2018 Computer Aided Verification. Springer, Cham. ISBN 9783319961446

[img] PDF - Accepted Version
Download (382kB)
[img] PDF - Published Version
Available under License Creative Commons Attribution.

Download (598kB)


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.

Item Type: Conference Proceedings
Keywords: software verification, Java, bounded model checking, SAT solving
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Peter Schrammel
Date Deposited: 22 May 2018 09:06
Last Modified: 08 Nov 2018 10:00
URI: http://sro.sussex.ac.uk/id/eprint/75980

View download statistics for this item

📧 Request an update