Open
Description
At a high level can one define a verification plan, where the available options are linked together abstractly. Try to apply the same idea for invariant generation. This seems to be of general importance in verification tools; can we build some generic infrastructure to support it?
Activity