JBMC

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

References in zbMATH (referenced in 2 articles )

Showing results 1 to 2 of 2.
Sorted by year (citations)

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Lucas Cordeiro, Daniel Kroening, Peter Schrammel: Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) (2018) arXiv