Find ODE conditions searches values that are necessary and sufficient to prove the post-condition. The tool produces two lists of formulas:

  1. The first list of formulas are the sufficient/necessary condition for the post-condition to be invariant
  2. The second list of formulas are necessary conditions for the safety question to be true at all with those assumptions
All formulas in the returned lists must be valid.

See also

Learning resources