VST-A: A Foundationally Sound Annotation Verifier for Imperative Programs

Explore a 19-minute conference talk from POPL 2024 introducing VST-A, a foundationally sound annotation verifier for imperative languages like C. Learn how VST-A combines the automation and convenience of annotation-based verifiers with the rich assertion language and formal soundness proofs of interactive verifiers. Discover how VST-A analyzes control flow graphs, decomposes C functions into control flow paths, and reduces program verification problems to straightline Hoare triples. Understand the advantages of VST-A's nonstructural decompositions and reductions compared to existing tools like VST and Iris. Gain insights into VST-A's implementation in Coq, including its soundness proof and call-by-value computation. Explore the system's ability to handle complex proof goals using the full power of the Coq proof assistant.

[POPL'24] VST-A: A Foundationally Sound Annotation Verifier