Treffer: JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)

Title:
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Authors:
Cordeiro, Lucas, Kroening, Daniel, Schrammel, Peter
Source:
Cordeiro, L, Kroening, D & Schrammel, P 2019, JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution). in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. https://doi.org/10.1007/978-3-030-17502-3_17
Publication Year:
2019
Collection:
The University of Manchester: Research Explorer - Publications
Document Type:
Fachzeitschrift article in journal/newspaper
Language:
English
DOI:
10.1007/978-3-030-17502-3_17
Availability:
https://research.manchester.ac.uk/en/publications/4255b8a7-4588-48d2-9cc5-421b341cb942
https://doi.org/10.1007/978-3-030-17502-3_17
Rights:
info:eu-repo/semantics/openAccess
Accession Number:
edsbas.EC221DD7
Database:
BASE

Weitere Informationen

JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.