Trabalho em anais de eventoOpen Access
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
CORDEIRO, L. C.; KESSELI, PASCAL; KROENING, DANIEL; SCHRAMMEL, P.; TRTIK, M
Resumo
Resumo
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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
palavras-chave
Palavras-chave
bounded model checkingprogram verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento