@agacek agacek released this Apr 30, 2018 · 4 commits to master since this release

Assets 3

Fixed a bug in IVC generation (issue #44)

@agacek agacek released this Jan 24, 2018 · 7 commits to master since this release

Assets 3
  • Added support for uninterpreted functions (see uf_*.lus files in testing directory)
  • Added -obfuscate flag to JLustre2Kind for obfuscating variable names in sensitive files
  • Updated PDR to only disable for individual non-linear properties (previously any non-linearities in a program disabled PDR)
  • Removed interval generalization
  • Add more utility functions to LustreUtil, NodeBuilder, and JKindResult
  • Various minor improvement and bug fixes

@agacek agacek released this Feb 22, 2017 · 53 commits to master since this release

Assets 3

JKind

  • Fix soundness bug with 'unknown' results during invariant generation for non-linear models

JKindApi

  • Ensure Excel workbooks are closed even if writing fails
  • Expose more subclass functionality in AnalysisResultLabelProvider.

@agacek agacek released this Nov 29, 2016 · 57 commits to master since this release

Assets 3

JKind

  • Changed multi-line comments from /* ... */ to (* ... *)
  • Return error code when an engine crashes
  • Check for inconsistency during base realizability checks
  • Fix default SMT solver in --help
  • Add -main option to specify main node
  • Add -no_slicing flag to disable slicing
  • Output warnings and errors on stderr instead of stdout

JKindApi

  • Terminate JKind gracefully from JKindApi
  • Add UI elements for inconsistent properties
  • Various other API improvements requested by users
  • Add JCoverage example using JKindApi and IVCs to determine coverage metrics

@agacek agacek released this Mar 25, 2016 · 83 commits to master since this release

Assets 3
  • Fix bug in type comparison for advice files
  • Pretty print time values, e.g. 2h 23m 48s
  • Change timeout and depth to be unbounded by default

@agacek agacek released this Mar 21, 2016 · 89 commits to master since this release

Assets 3

The big focus of JKind v3.0 is bundling and ease-of-use. The default solver has changed from Yices to SMTInterpol. This means users will no longer need to install an SMT solver by default. In addition, JKindApi has been updated to make it possible to bundle JKind into existing applications. Tools like AGREE, Spear, and JKind-Xtext have been updated to bundle JKind. Thus tool users won't need to install JKind or any SMT solvers. Everything will work out of the box.

Other notes

  • Added LustreParseUtil to allow JKindApi users to specify ASTs using concrete syntax together with substitutions for variables.
  • Error messages about the input Lustre now display and highlight the relevant portion of the input file.
  • "Set of support" has been renamed to "inductive validity core." This now uses the annotation --%IVC and the flag -ivc.
  • Enabled smoothing for Z3.
  • Shell scripts now work on Linux and OS X (Thanks to Dave Greve).
  • BigFraction.doubleValue() is now stable for large fractions (Thanks to Dave Greve).
  • Added EquationBuilder.
  • Added JLustre2ExcelApi.

@agacek agacek released this Dec 17, 2015 · 107 commits to master since this release

Assets 3
  • 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.

Oct 23, 2015
fixing bug in sexp conversion
Sep 14, 2015
adding in the multi solver

@agacek agacek released this Aug 20, 2015 · 141 commits to master since this release

Assets 3
  • Fix bug in reconstruction of inductive counterexamples (Thanks to Steve Miller for finding this).
  • Support for mod and div in Yices 2 now that Yices 2.4.1 supports those operators
  • Check <SOLVER>_HOME/bin and <SOLVER>_HOME for solver executables