There are various kinds of static (and dynamic) verification frameworks and tools, all with weaknesses and strengths. Combining them manually or automatically is common by making different tools interoperate or integrating various analyses in the same tool. In SPARK, two analyses work on different paths: deductive verification and data and information flow analysis. This talk presents how these analyses collaborate to improve the efficiency and precision of the SPARK tool while retaining soundness.