JayHorn View project on GitHub

JayHorn Overview.

JayHorn is a software model checking tool for Java. JayHorn uses the Java optimization framework Soot as a front-end, generates a set of constrained Horn clauses (CHCs) to encode the verification condition. The Horn clauses are then sent to a Horn engine. For the construction of JayHorn we made the following design decisions:

1. Perform as much of the translation work as possible in Soot: Translation of exception handling, de-virtualization, and control-flow simplification are implemented as bytecode transformation. These steps do not alter a programs behavior which allows us to use testing to check their correctness.

2. Keep the glue code that generates verification conditions small, modular, and extensible: by performing many steps as bytecode transformation, the step of generating verification conditions becomes relatively simple and is implemented in a few hundred lines of Java code. The implementation is modular and extensible to allow, for example, different encoding of memory or numeric types.

3. Keep the back-end exchangeable: Horn solvers are constantly improving and new tools are being released frequently. To ensure that JayHorn builds on the most efficient back-end, we made it modular and replaceable. Currently, JayHorn supports Z3, Eldarica, and Spacer as back-ends but can be easily extended to support other tools.

For more details read our CAV 2016 tool paper.

*NEW* Read the war stories from the development of JayHorn in our new blog.

Obtaining JayHorn

JayHorn does not have a stable release yet. Take a look at our releases to get the latest version and instructions how to run it. All current releases are known to be unsound due to bugs or missing features, so don't use them to verify things that may explode.