Skip to content

JKind v2.0
Compare
Choose a tag to compare
@agacek agacek released this 11 Dec 18:52
· 294 commits to master since this release
v2.0
0d6b10c

JKind has now hit version 2. This version packs some exciting new
features like property directed reachability and improved
re-verification.

This version should be compatible with the previous version of
JKind-API, though developers are still recommended to upgrade their
tools to the latest JKind-API.

Property Directed Reachability (PDR)

JKind now supports property directed reachability (PDR). PDR is very
powerful and can solve many model checking problems that elude
k-induction. Moreover, PDR produces invariants which k-induction can
use, thus the two techniques work well together.

PDR works best by focusing on a single property at a time. We handle
multiple properties by spawning parallel PDR instances and working on
the properties sequentially. The best number of instances to use is
still being investigated. More PDR instances means more problems can
potentially be solved sooner, but it also consumes more of the CPU
thus taking time away from k-induction and the other PDR instances. We
currently use 1 PDR instance for 4 core machines and 2 PDR instances
for 8 cores machines. This value can be modified using the -pdr_max
command line flag. We are interested in feedback about what values
work best for this setting.

Our implementation of PDR is based on "Efficient Implementation of
Property Directed Reachability" by Niklas Een, Alan Mishchenko, and
Robert Brayton. The extension to SMT is based on "IC3 Modulo Theories
via Implicit Predicate Abstraction" by Alessandro Cimatti, Alberto
Griggio, Sergio Mover, and Stefano Tonetta. The underlying solver is
SMTInterpol by Jochen Hoenicke, Jürgen Christ, and Alexander
Nutz. This solver is bundled into JKind.

Improved Re-verification (advice)

JKind has the ability to remember invariants from previous runs and to
use them to speed up future runs. This mechanism is called advice.
When you run JKind with the -write_advice <filename> command line
flag it will store a record of proven invariants in the given file. If
you then run JKind with -read_advice <filename> it will use that
file to speed up verification.

For most problems, advice significantly speeds up re-verification
time, often by a order of magnitude or more. For example, anything
proven by PDR will produce an advice file which can be checked almost
instantly. Some problems, however, simply require a large value of k
in k-induction. So even with the invariants provided by advice, the
re-verification time may not be improved.

Advice is transportable. If you change your property or even your
system, you can still use a previous advice file for it. JKind never
trusts the advice it receives and always attempts to re-verify it. It
will filter out invariants that are no longer well-formed (due to
missing variables or different types), and it will attempt to re-verify
whatever is left. In some cases, the remaining invariants may still be
useful enough to shorten verification time.

We are interested in feedback about experiences with advice.

SMTInterpol

JKind now supports the SMTInterpol solver. This is a Java-based SMT
solver, and thanks to its LGPL license it is bundled with JKind. That
means JKind can run without a external solver by using the -solver smtinterpol flag.

Other Changes

  • JKind (and JKind-API) now require Java 8. If you get an error about
    major/minor version numbers, you are running an older version of
    Java.
  • When JKind detects that it is being killed, it will do its usual
    final processing including printing inductive counterexamples and
    displaying a summary.
  • Variables of enumeration and subrange types are now assumed to be
    type correct even in the pre-initial state. That is, if you refer to
    the previous value of such a variable in the initial state, the
    result will be type safe. This matches the behavior of Kind 2.
  • Invariant generation is now allowed to prove properties directly.
  • JKind now supports MathSAT for problems that don't use integer
    division or modulo.
  • Fixed bug in the reporting of progress when post-processing of
    counterexamples is enabled (e.g. smoothing or interval
    generalization).
  • Command line options and JKindApi options have changed slightly in
    some cases to allow specific proving engines to be disabled.
  • Fixed bug in parsing of right associative operators.
  • JKind can now directly execute the output of JLustre2Kind.
Assets 3
Loading