JBMC: Bounded Model Checking for Java Bytecode Article Swipe

PDF

Related Concepts

Computer science Java bytecode Programming language Bytecode Java Model checking Bounded function Java Modeling Language Java applet Recursion (computer science) Java annotation Set (abstract data type) Generics in Java Theoretical computer science Operating system Mathematics Mathematical analysis

Lucas C. Cordeiro , Daniel Kroening , Peter Schrammel ·

YOU? · · 2019 · Open Access · · DOI: https://doi.org/10.1007/978-3-030-17502-3_17 · OA: W2913717796

JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.