JKind v2.1.1

This is a minor release which fixes various bugs:

• Fix possible looping behavior during cycle detection
• Reduce number of state variables used when translating condacts
• More sophisticated handling of 'unknown' properties
• Switch to simpler Z3 check-sat interface for non-linear problems
• Fix race condition between BMC check and user output

JKind v2.1

This release introduces JRealizability which is a program to check realizability of a Lustre file. This work is based on our our recent research and on code developed by Andreas Katis. Examples of realizability are available in the repository.

This release also fixes a bug with nested pre operators within condacts.

JKind v2.0.1

This release fixes a bug in PDR which could cause JKind to crash.

JKind v2.0

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.

JKind v1.6.1

Features

• The XML file now contains progress messages from the BMC process. JKind-API now makes use of this information in the results view.
• New graphical counterexample UI available in JKind-API
• JKind now has meaningful exit codes

Fixes

• Eagerly open xls files for writing to prevent delayed error messages
• Handle record and array types in NodeLayout
• Check that array sizes are not too large
• Fix linear check with respect to solvers
• Be more persistent about unknown results in inductive process

JKind v1.6

Features

• New backend SMT translation avoids uninterpreted functions. In general, this means much better performance for larger/harder models.
• Support for Yices 2 (using yices-smt2 executable).
• Support for Kind 2 (local and remote) in JKind API.
• Improved invariant generation for integers with fixed initial values.
• Support for JKIND_HOME, YICES_HOME, YICES2_HOME, Z3_HOME, and CVC4_HOME environment variables for users who do not want to put JKind or their SMT solvers in their PATH.
• New NodeBuilder and ProgramBuilder objects in JKind API to make it easier to construct nodes and programs in an imperative style.

Fixes

• Fix bug in model evaluation related to subtraction
• Improved error messages for bad file name inputs

JKind v1.5.2

Fixes

• Fix bug in printing of enumerated types
• Fix bug where enumerated values were not treated as constants by static analysis
• Fix non-termination bug in constant evaluation
• Fix bracket encoding bug in jlustre2kind
• Fix encoding of invariants in XML output
• Exit with error when record fields are repeated
• Fix null pointer exception when diving by a variable

JKind v1.5.1

Features

• Added enumeration types, for example

type state = enum { A, B, C, Error };

• Added Turing machine example.
• Users of the JKind API may now pass null to AST constructors
  in place of empty lists.
• Added -xml_to_stdout flag which prints results as an xml file
  directly to the standard output.
• Allow types and constants to reference previous types and constants
  rather than requring declaration before use.

Changes

• We no longer support equations with no left-hand side. Instead, one
  must at least use () as the left-hand side when an equation assigns
  no variables.
• Constants and enumeration literals must have globally unique names
  (e.g. cannot conflict with node variables).

Fixes

• Added support for 'unknown' result from Z3.
• Improved parsing performance.
• Fixed bug in tuple handling.
• Fixed unguarded pre check with respect to node calls.
• Fixed integer overflow error with bounds checking for arrays.

JKind v1.5

Features

• Detect (some) duplicate node calls and coalesce them for efficiency
• From Lucas Wagner: support for tuples so that multi-return node calls can occur
  anywhere in an expression. For example:

  flag, value = if a > b then nodecall(x) else (true, 0)

• Support for int/real casting using real(x) and floor(x)
• Support for non-linear arithmetic when using Z3. This requires disabling the checks for division by zero, modulus by a negative integer, and integer division by a negative integer. The behavior under any of these conditions is left unspecified and subject to change in the future.
• Added JKindApi.setSolver() (options: Yices, Z3, CVC4)

Feature: Record Updates

From Lucas Wagner: this release adds support for record updates using the syntax expr{field := value}. This is a functional update so it returns a new record with the updated value rather than changing the original record. The precedence of pre and record update may be initially confusing. Note the following equivalences

  pre expr{field := value} ==> (pre expr){field := (pre value)}
  pre(expr){field := value} ==> (pre expr){field := (pre value)}

Thus one should use (pre ...) to ensure the proper scope for pre expressions when using record updates.

Feature: Arrays

This release adds support for arrays. For example:

var
  A : int[5];
  sorted : bool;
let
  A = [0, 0, 0, 0, 0] -> (pre A)[i := v]
  sorted = A[0] <= A[1] and A[1] <= A[2] and ...;

Arrays are currently expanded to scalars, and dynamic indexing into
arrays for lookup or update is expanded to if-then-else expressions. Array updates are functional, just like record updates. Also, the precedence of pre and array lookup and update may be initially confusing. Note the following equivalences

  pre A[i := v] ==> (pre A)[(pre i) := (pre v)]
  pre(A)[i := v] ==> (pre A)[(pre i) := (pre v)]
  pre A[i] ==> (pre A)[pre i]
  pre(A)[i] ==> (pre A)[pre i]

Thus one should use (pre ...) to ensure the proper scope for pre expressions when using array operations.

Indexing outside of array bounds is discouraged. The current behavior for updates outside of array bounds is that they are ignored. The current behavior for lookups outside of arrays bound is that they return a default value. Both of these behaviors are subject to change in the future and should not be relied upon.

Fixes

• Fixed bug in constant inlining which would cause some constants not be inlined
• Fixed bug in checking for division by zero within constant declarations
• Fixed bug in the options sent to CVC4 so that integer division by a constant is supported
• Fixed bug in counterexample reconstruction which could crash JKind

JKind v1.4.5

Fixes

• Fixed bug in lookup of partial functions returned by Yices (discovered by Lucas Wagner)
• Fixed bug in pretty-printing of subrange int types (discovered by Dan DaCosta)
• Fixed bug in type checking for records (discovered by Dan DaCosta)
• Fixed bug in evaluation of 'and' expressions