Two-way collaboration between flow and proof in SPARK
summary
SPARK (AdaCore) implements a two‑way integration where a fast interprocedural data+information flow pass runs first to emit approximated global contracts, call graphs and termination flags, and a later deductive verification pass generates SMT verification conditions to prove dead branches, loop variants and value‑dependent initialization. A new relaxed initialization option tags objects or parameters so proof tracks per‑field initialized flags while flow still enforces strict cases; this increases precision, is mostly automated, preserves soundness and trades slower SMT solving and heavier contracts for fewer false positives.
AI-written summary · about
chapters (9)
- 0:00SPARK introduction
- 3:54What SPARK verifies
- 7:47Flow analysis limits
- 10:17Flow supports proof
- 13:30Proof analysis
- 16:47Automated flow-proof
- 17:51Relaxed initialization
- 23:31Flow-proof summary
- 24:13Q&A
related talks
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
15mAutomatic Synthesis of Data-Flow Analyzers
01h 05mVerifying Infinitely Many Programs at Once
29mQ: A Sound Verification Framework for Statecharts and Their Implementations
19mProof Automation for Linearizability in Separation Logic
15mCorrectness-by-Construction for Feature-Oriented Software Product Lines
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
23mFireside Chat