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
![]() |
PDF
- Accepted Version
Download (382kB) |
![]() |
PDF
- Published Version
Available under License Creative Commons Attribution. Download (598kB) |
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.
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