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
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Lucas Cordeiro, Daniel Kroening, Peter Schrammel: Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) (2018) arXiv