Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-96145-3_10 | COMPUTER AIDED VERIFICATION (CAV 2018), PT I |
Field | DocType | Volume |
Model checking,Programming language,Computer science,Theoretical computer science,Java bytecode,Java,Bounded function,Software verification | Conference | 10981 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.36 |
References | Authors | |
9 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lucas Cordeiro | 1 | 360 | 38.38 |
| Pascal Kesseli | 2 | 11 | 1.59 |
| Daniel Kroening | 3 | 3084 | 187.60 |
| Peter Schrammel | 4 | 134 | 19.10 |
| Marek Trtík | 5 | 1 | 0.36 |