Independent proof obligations

[sjcjoosten]

For speeding up verification, proof goals can be split up into separately verifiable viper files. The viper output of those files can then be cached, such that when the verification is done again, it does not take any extra time.

As this issue gives rise to a bunch of ideas, I suggest we close this issue as soon as some form of splitting proof obligations is implemented (and it works). Other steps we could take:

• [ ] Splitting verification of contracts for pure methods and other things that are sometimes inlined and sometimes not (method bodies are never inlined, so it's easier to start with those)
• [ ] Finer or courser granularity of splitting proof goals: one verification condition at a time, one method body at a time, one class at a time, or splitting through user flags/annotations.
• [ ] Cache each proof goal: write (a hash of) the Viper file to some cache directory and if it is unchanged, don't re-check it.
• [ ] Parallel proof goals: verify proof goals in parallel (using separate threads)