Treffer: JBMC: a bounded model checking tool for verifying java bytecode
Title:
JBMC: a bounded model checking tool for verifying java bytecode
Publisher Information:
Springer
Publication Year:
2018
Collection:
University of Sussex: Sussex Research Online
Subject Terms:
Document Type:
Konferenz
conference object
File Description:
application/pdf
Language:
English
Relation:
http://sro.sussex.ac.uk/id/eprint/75980/1/cav2018-jbmc.pdf; http://sro.sussex.ac.uk/id/eprint/75980/3/Cordeiro2018_Chapter_JBMCABoundedModelCheckingToolF.pdf; 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
DOI:
10.1007/978-3-319-96145-3_10
Availability:
Rights:
cc_by_4
Accession Number:
edsbas.CE344CD5
Database:
BASE
Weitere Informationen
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.