I am trying to understand the concept of delayed abstraction mentioned in paper [416] at: Link of VerX
VerX tool uses the concept of delayed abstraction for SC verification. Is Delayed abstraction related to automatic generation of abstractions? I can’t unerstand this concept:
To verify a Past LTL specification of a bundle of contracts C we apply abstract interpretation over a symbolic domain. We employ predicate abstraction [35] but without the usual conversion to boolean programs. Our approach is similar to that of Flanagan and Qadeer [32] where two transformers are alternated: precise symbolic transformers to handle individual commands, and an imprecise transformer to ensure convergence. In contrast, classic abstraction applies an imprecise transformer at every step. Hence, we call the precise/imprecise approach delayed abstraction.
Somebody please guide me. Zulfi.
