{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:24:58Z","timestamp":1770279898522,"version":"3.49.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF China","award":["61902240"],"award-info":[{"award-number":["61902240"]}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["HR001120C0160"],"award-info":[{"award-number":["HR001120C0160"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Program verifiers for imperative languages such as C may be\n            <jats:italic toggle=\"yes\">annotation-based<\/jats:italic>\n            , in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are\n            <jats:italic toggle=\"yes\">interactively<\/jats:italic>\n            developed in a proof assistant such as Coq. Annotation verifiers have been more automated and convenient, but some interactive verifiers have richer assertion languages and formal proofs of soundness. We present VST-A, an annotation verifier that uses the rich assertion language of VST, leverages the formal soundness proof of VST, but allows users to describe functional correctness proofs intuitively by inserting assertions.\n          <\/jats:p>\n          <jats:p>\n            VST-A analyzes control flow graphs, decomposes every C function into control flow paths between assertions, and reduces program verification problems into corresponding\n            <jats:italic toggle=\"yes\">straightline Hoare triples<\/jats:italic>\n            . Compared to existing foundational program verification tools like VST and Iris, in VST-A such decompositions and reductions can nonstructural, which makes VST-A more flexible to use.\n          <\/jats:p>\n          <jats:p>VST-A\u2019s decomposition and 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 VST\u2019s 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.<\/jats:p>","DOI":"10.1145\/3632911","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2069-2098","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["VST-A: A Foundationally Sound Annotation Verifier"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3046-7085","authenticated-orcid":false,"given":"Litao","family":"Zhou","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"},{"name":"University of Hong Kong, Hong Kong, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1581-9577","authenticated-orcid":false,"given":"Jianxing","family":"Qin","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6486-3409","authenticated-orcid":false,"given":"Qinshi","family":"Wang","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5678-6538","authenticated-orcid":false,"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Patrick Baudin Fran\u00e7ois Bobot David B\u00fchler Lo\u00efc Correnson Florent Kirchner Nikolai Kosmatov Andr\u00e9 Maroneze Valentin Perrelle Virgile Prevosto Julien Signoles and Nicky Williams. 2021. The dogged pursuit of bug-free C programs: The Frama-C Software Analysis Platform. 56\u201367 pages. https:\/\/doi.org\/10.1145\/3470569 10.1145\/3470569","DOI":"10.1145\/3470569"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_5"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.camwa.2014.06.004"},{"key":"e_1_3_1_10_1","unstructured":"Pierre Boutillier Stephane Glondu Benjamin Gr\u00e9goire Hugo Herbelin Pierre Letouzey Pierre-Marie P\u00e9drot Yann R\u00e9gis-Gianas Matthieu Sozeau Arnaud Spiwack and Enrico Tassi. 2014. Coq 8.4 Reference Manual. (jul 2014). https:\/\/hal.inria.fr\/hal-01114602"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_14"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3642-20398-5_33"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9457-5"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632902"},{"key":"e_1_3_1_17_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H","year":"2022","unstructured":"Thomas H Cormen, Charles E Leiserson, Ronald L Rivest, and Clifford Stein. 2022. Introduction to Algorithms. MIT press."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371101"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3642-37036-6_8"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/97894-011-1793-7_4"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.021"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-014-0164-0"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_31"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3158196"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Ike Mulder Robbert Krebbers and Herman Geuvers. 2022. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris. (2022) 16. https:\/\/doi.org\/10.1145\/3519939.3523432 10.1145\/3519939.3523432","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_1"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2002.1029817"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_40_1","first-page":"343","volume-title":"The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013","author":"Turon Aaron Joseph","year":"2013","unstructured":"Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for finegrained concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 343\u2013356. https: \/\/doi.org\/10.1145\/2429069.2429111"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Zhongye Wang Qinxiang Cao and Yichen Tao. 2023. Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding. https:\/\/doi.org\/10.48550\/arXiv.2310.17616 10.48550\/arXiv.2310.17616 arXiv:2310.17616 [cs.PL]","DOI":"10.48550\/arXiv.2310.17616"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_27"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_2"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1909.00097"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10207523"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632911","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632911","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:03Z","timestamp":1751659623000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632911"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632911"],"URL":"https:\/\/doi.org\/10.1145\/3632911","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}