A²I: abstract² interpretation.

ion of the maximal trace semantics of A: SprJAKX 0 ≜ αpr(SmJAKX ) = αpr(αm(SpfJAKX )) ∈ Dpr(X ) ≜ (∏ni=1(Di )+ω+1)(X ) This projection semantics can be characterized as limit of the transfinite iterates of the following function Fpr(X ): Fpr(X ) ∈ Dpr(X ) −→ Dpr(X ) (13) Fpr(X ) Û X ≜   Û X · Fk+1( Û X k ) if ∃k ∈ N . Û X ∈ ∏ni=1(Di )k ∧ itpr( Û X ) Û X · Û X k if ∃k ∈ N . Û X ∈ ∏ni=1(Di )k ∧ stpr( Û X ) Û X · Û Xω if Û X ∈ ∏ni=1(Di )ω ∧ wbpr( Û X ) ∧ Û Xω = Fω( Û X )