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...

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron: Cordeiro, L, Kesseli, P, Kroening, D, Schrammel, P, Trtik, M
Fformat: Conference item
Cyhoeddwyd: Springer, Cham 2018

Eitemau Tebyg