Building a competitive program verifiers is becoming cheaper.  On the
front-end side, openly available compiler infrastructure and
optimization frameworks take care of hairy problems such as alias
analysis, and break down the subtleties of modern languages into a
handful of simple instructions that need to be handled. On the
back-end side, theorem provers start providing full-fledged model
checking algorithms, such as PDR, that take care looping control-flow.
In this spirit, we developed JayHorn, a verification framework for
Java with the goal of having as few moving parts as possible. Most
steps of the translation from Java into logic are implemented as
bytecode transformations, with the implication that their soundness
can be tested easily. From the transformed bytecode, we generate a set
of constrained Horn clauses that are verified using state-of-the-art
Horn solvers. We report on our implementation experience and evaluate
JayHorn on benchmarks.