Two-way Collaboration Between Flow and Proof in SPARK

Explore a 29-minute conference presentation from VMCAI 2025 that examines the collaborative relationship between deductive verification and data/information flow analysis in the SPARK verification tool for Ada language. Learn how these two static analyses work together to provide stronger guarantees while reducing manual effort. The speakers—Claire Dross, Joffrey Huguet, and Johannes Kanig from AdaCore—demonstrate how verification responsibilities are distributed between these analyses to maximize their potential, improving both efficiency and precision while maintaining soundness. The presentation highlights automated collaborations between the analyses and explains a feature allowing users to choose which analysis verifies initialization based on their preferred trade-offs. This talk was presented at the VMCAI conference in January 2025 and sponsored by ACM SIGPLAN.