Verifying aspect advice modularly