JBMC

Bounded model-checker for Java (bytecode), verifies user-defined assertions, standard assertions, several coverage metric analyses.

https://www.cprover.org/jbmc/

https://github.com/peterschrammel/cbmc/releases/tag/jbmc-5.8-cav18

Open Source

Maintained