search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Confusions about the verification result #71

Closed verifierlife closed 2 years ago

verifierlife commented 2 years ago

If there are too many variables and equations in Lustre program, some results confuse me.

  1. The translation step prompts “OutOfMemoryError”. Monitoring tools show that the memory in old generation of JVM is full.
  2. The solving step prompts “OutOfMemoryError”.
  3. The solving step keep running without stop.
  4. A relatively good result may be "Unknown Property" without some illustration to explain it. However, the same property in the same Lustre program appears "Valid" or "Invalid" after trying a computer with lager memory.

It will be inspiring if the above confusions can be improved.

(ps. Windows OS with 8G/16G/32G memory, solvers: smtinterpol, z3, mathsat, cvc (All are the latest release)).

lgwagner commented 2 years ago

I have been in discussions with this user via email and have helped them troubleshoot this as well as I can.

The user has a very large model with hundreds (perhaps thousands) of inputs and that is challenging JKind in the translation step and solving step. The user will have to skillfully employ some abstractions in their model and/or use compositional reasoning to get to a conclusive proof result as it is much too large to be solved by JKind as is.

One thing that could be done is an upfront estimation / guesstimation that a model is likely too large to be successfully analyzed. That would have to be based on number of true inputs and would only be a heuristic. That way a user would have some indication that they are unlikely to be successful using JKind for their problems and help in setting the correct expectations from the tool.