Skip to main content

Trabalho em anais de eventoOpen Access

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

CORDEIRO, L. C.; KROENING, D.; SCHRAMMEL, P

2019 • 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems • 23 citações

Resumo

Resumo

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.

palavras-chave

Palavras-chave

bounded model checkingJava bytecodeJava standard libraryverification conditionsMiniSatassertionCBMC

Status

Published

links

Trabalho em anais de evento