Skip to content

JKind v2.3
Compare
Choose a tag to compare
@agacek agacek released this 17 Dec 17:51
· 212 commits to master since this release
v2.3
1e95315
  • From Elaheh Ghassabani: add new -support flag and corresponding --%SUPPORT annotation. See below for details.
  • Use truncated decimal values instead of fractions for console output.
  • Add note to truncated decimal values in Excel output.
  • Move some Lustre translation passes so they are visible in JKindApi.
  • Add debug option to JKindApi which causes intermediate files to be saved and commands to be logged.
  • Display detected SMT solvers when run with -version flag.
  • Flush XML file only after major events to prevent file system strain.

Support

The new -support flag in JKind causes two things for each valid property. First, the set of invariants used to prove the property is reduced and reported (thus replacing the -reduce_inv flag). Second, any variables listed in a --%SUPPORT annotation are analyzed to see if the equations for those variables are necessary to prove the property and its reduced set of invariants. The set of necessary variable equations is reported.

Assets 3
Loading