Conference item
JBMC: a bounded model checking tool for verifying Java bytecode
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 584.7KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-319-96145-3_10
Authors
- Publisher:
- Springer, Cham
- Host title:
- CAV 2018: Computer Aided Verification
- Journal:
- Lecture Notes in Computer Science More from this journal
- Volume:
- 10981
- Pages:
- 183-190
- Series:
- Lecture Notes in Computer Science
- Publication date:
- 2018-07-18
- Acceptance date:
- 2018-03-31
- Event location:
- Oxford, UK
- DOI:
- ISSN:
-
0302-9743
- ISBN:
- 9783319961453
- Pubs id:
-
pubs:835638
- UUID:
-
uuid:ecbf0b6e-1b76-4fd2-8f89-c90f9bcfe6dd
- Local pid:
-
pubs:835638
- Source identifiers:
-
835638
- Deposit date:
-
2018-04-14
- ARK identifier:
Terms of use
- Copyright holder:
- Cordeiro et al
- Copyright date:
- 2018
- Notes:
-
Copyright © 2018 The Authors. This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record