PV4 ⊧ JayHornchecks user-specified assertions and infers some annotations for Java programs

JayHorn is a model checker for verifying the absence of assertion violations in sequential Java programs by automatically inferring program annotations that are sufficient to witness program safety

Application domain/field

• Model checking
• Sequential programs
• Safety verification
• Software model checking

Type of tool

Model checker

Expected input

Program with assertions

Format:

Java bytecode (it supports Java class files, Jar archives, or Android apk)

Expected output

SAFE, UNSAFE or UNKNOWN

Internals

Uses Eldarica, Spacer as back-end solvers and Soot to translate Java bytecode to simplified Jimple three-address format. JayHorn can also infer some program annotations automatically for NullPointerExceptions, ArrayIndexOutOfBoundsExceptions and ClassCastExceptions.

Comments

JayHorn does not support strings, enums, bounded integer data-types, floating-point data-types, reflection, dynamic loading, and concurrency License: MIT