• JBMC: a bounded model checking...

Treffer: JBMC: a bounded model checking tool for verifying java bytecode

Title:
JBMC: a bounded model checking tool for verifying java bytecode
Authors:
Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, Marek Trtik
Publication Year:
2018
Collection:
University of Sussex (US): Figshare
Subject Terms:
software verification, Java, bounded model checking, SAT solving
Document Type:
Konferenz conference object
Language:
unknown
Relation:
10779/uos.23457887.v2; https://figshare.com/articles/conference_contribution/JBMC_a_bounded_model_checking_tool_for_verifying_java_bytecode/23457887
Availability:
https://figshare.com/articles/conference_contribution/JBMC_a_bounded_model_checking_tool_for_verifying_java_bytecode/23457887
Rights:
CC BY 4.0
Accession Number:
edsbas.F48DFBCD
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.