JBMC: a bounded model checking tool for verifying Java bytecode
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 resul...
Бүрэн тодорхойлолт
Номзүйн дэлгэрэнгүй
Үндсэн зохиолчид: |
Cordeiro, L,
Kesseli, P,
Kroening, D,
Schrammel, P,
Trtik, M |
Формат: | Conference item
|
Хэвлэсэн: |
Springer, Cham
2018
|