VST-A: A Foundationally Sound Annotation Verifier
summary
VST-A is an annotation verifier that parses C into control‑flow graphs, splits functions into paths (four paths for the linked‑list reverse example) and reduces verification to straightline Hoare triples that are proved sound in Coq; the split and reduction are computed call‑by‑value in Coq and their soundness is a pure logical proof independent of VST’s complicated semantic model. It supports non‑structural proofs (generalized loop invariants, omitted join conditions), forbids ghost updates until handled, requires precise function specs, and ships evaluated artifacts with comparisons showing similar or lower proof effort on lists and a small interpreter.
AI-written summary · about