JBMC is a Bounded Model Checker for Java programs. It checks runtime exceptions and user-definded assertions. The verification is performed by unwinding the loops in the program and passing the resulting formula to a decision procedure.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element