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:
- Generate VC's from the program.
- Solve it: If user provide inductive invariants just check the Validity of the whole VC formula.
- 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.