Skip to content

JKind 4.2.0
Compare
Choose a tag to compare
@lgwagner lgwagner released this 11 Jun 18:29
· 84 commits to master since this release
v4.2.0
42ca5a1

JKind now supports the enumeration of all minimal inductive validity Cores (All-MIVCs) to provide a complete enumeration of all minimal sets of model elements necessary for inductive proofs of a safety property. To compute All-MIVCs, run JKind with the following arguments:

-all_ivcs -solver z3

Users may use the -timeout argument to limit the time for the All-MIVCs computation. If the computation times out, the results may be incomplete and an warning is printed to the standard and xml output formats.

-timeout 1800

Requirements: All-MIVCs is verified to work with solvers Z3 (versions 4.5.0 or later)

Assets 3
Loading