As far as i can understand the problem of checking safety property, can be reduce to solving for inductive invariants in VC's and there is following parts to it:

  1. Generate VC's from the program.
  2. Solve it: If user provide inductive invariants just check the Validity of the whole VC formula.
  3. Inferring problem : simultaneously solve the VC's taking these predicates as uninterpreted function that make all the VC's valid.

How hard the problem of checking 2. (User provide the inductive invariant) in the case of array theory? For example: Array sorting.

  • 1
    $\begingroup$ I don't understand what you are asking. What relations are you referring to? Checking validity of the formula is undecidable. What is your question? Requests for software tools are off-topic here. $\endgroup$ – D.W. Apr 24 '17 at 12:05
  • $\begingroup$ By relations i mean Inductive invariants. $\endgroup$ – Pushpa Apr 24 '17 at 12:45

Sure, if the user provides inductive invariants, you can try to check the validity of the verification conditions. However, this remains undecidable, as it requires checking the validity of a formula in first-order logic (with quantifiers and array expressions), and that's undecidable.

It might be feasible often enough in practice to be useful, especially since we might hope that programmers have a reason why their code is correct and won't write code that requires overly complex reasoning to prove correct. But in general, it is undecidable.

  • $\begingroup$ Thanks. A follow up does't sortedness property be handles by array property fragment ? which is decidable ? $\endgroup$ – Pushpa Apr 24 '17 at 16:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.