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...
| المؤلفون الرئيسيون: | , , , , |
|---|---|
| التنسيق: | Conference item |
| منشور في: |
Springer, Cham
2018
|
| _version_ | 1826303436870647808 |
|---|---|
| author | Cordeiro, L Kesseli, P Kroening, D Schrammel, P Trtik, M |
| author_facet | Cordeiro, L Kesseli, P Kroening, D Schrammel, P Trtik, M |
| author_sort | Cordeiro, L |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T06:02:40Z |
| format | Conference item |
| id | oxford-uuid:ecbf0b6e-1b76-4fd2-8f89-c90f9bcfe6dd |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:02:40Z |
| publishDate | 2018 |
| publisher | Springer, Cham |
| record_format | dspace |
| spelling | oxford-uuid:ecbf0b6e-1b76-4fd2-8f89-c90f9bcfe6dd2022-03-27T11:19:50ZJBMC: a bounded model checking tool for verifying Java bytecodeConference itemhttp://purl.org/coar/resource_type/c_5794uuid:ecbf0b6e-1b76-4fd2-8f89-c90f9bcfe6ddSymplectic Elements at OxfordSpringer, Cham2018Cordeiro, LKesseli, PKroening, DSchrammel, PTrtik, M 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. |
| spellingShingle | Cordeiro, L Kesseli, P Kroening, D Schrammel, P Trtik, M JBMC: a bounded model checking tool for verifying Java bytecode |
| title | JBMC: a bounded model checking tool for verifying Java bytecode |
| title_full | JBMC: a bounded model checking tool for verifying Java bytecode |
| title_fullStr | JBMC: a bounded model checking tool for verifying Java bytecode |
| title_full_unstemmed | JBMC: a bounded model checking tool for verifying Java bytecode |
| title_short | JBMC: a bounded model checking tool for verifying Java bytecode |
| title_sort | jbmc a bounded model checking tool for verifying java bytecode |
| work_keys_str_mv | AT cordeirol jbmcaboundedmodelcheckingtoolforverifyingjavabytecode AT kesselip jbmcaboundedmodelcheckingtoolforverifyingjavabytecode AT kroeningd jbmcaboundedmodelcheckingtoolforverifyingjavabytecode AT schrammelp jbmcaboundedmodelcheckingtoolforverifyingjavabytecode AT trtikm jbmcaboundedmodelcheckingtoolforverifyingjavabytecode |