JayHorn is a model checker for verifying sequential Java programs
  annotated with assertions expressing safety conditions. JayHorn
  uses the Soot library to read Java bytecode and translate it to the
  Jimple three-address format, then converts the Jimple 
  code in several stages to a set of constrained Horn clauses, and
  solves the Horn clauses using solvers like Spacer and Eldarica. JayHorn
  uses a novel, invariant-based representation of heap
  data-structures, and is therefore particularly useful for analyzing
  programs with unbounded data-structures and unbounded
  run-time. JayHorn is open source and distributed under MIT
  license.