Cordeiro2018_Chapter_JBMCABoundedModelCheckingToolF.pdf (584.7 kB)
JBMC: a bounded model checking tool for verifying java bytecode
Version 2 2023-06-12, 07:22
Version 1 2023-06-09, 13:24
conference contribution
posted on 2023-06-12, 07:22 authored by Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, Marek TrtikWe 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.
History
Publication status
- Published
File Version
- Published version
Journal
CAV 2018 Computer Aided VerificationPublisher
SpringerExternal DOI
Event name
CAV 2018- 30th International Conference on Computer Aided VerificationEvent location
Oxford, UKEvent type
conferenceEvent date
July 14-17, 2018Place of publication
ChamISBN
9783319961446Series
Lecture Notes in Computer ScienceDepartment affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2018-05-22First Open Access (FOA) Date
2018-07-24First Compliant Deposit (FCD) Date
2018-05-19Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC