[G] Foundationally sound annotation verifier via control flow splitting
We propose VST-A, a new framework for program verification, based on the idea of reducing large program proofs into simpler verification goals. This new approach combines the benefits of interactive provers as well as the readability of annotated programs, and enables incremental program verification for incremental program development. VST-A analyzes control flow graphs and reduces the program verification problem to the verification of each control flow path between assertions. This reduction is defined in Coq, proved sound in Coq, and computed call-by-value in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of its underlying Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.