Conference item icon

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
Version:
Publisher's version

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-319-96145-3_10

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Kesseli, P More by this author
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Schrammel, P More by this author
Publisher:
Springer, Cham Publisher's website
Volume:
10981
Pages:
183-190
Series:
Lecture Notes in Computer Science
Publication date:
2018-07-18
Acceptance date:
2018-03-31
DOI:
ISSN:
0302-9743
Pubs id:
pubs:835638
URN:
uri:ecbf0b6e-1b76-4fd2-8f89-c90f9bcfe6dd
UUID:
uuid:ecbf0b6e-1b76-4fd2-8f89-c90f9bcfe6dd
Local pid:
pubs:835638
ISBN:
978-3-319-96145-3

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP