{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:47:33Z","timestamp":1773193653379,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683289,789108"],"award-info":[{"award-number":["683289,789108"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (\n            <jats:italic>e.g.<\/jats:italic>\n            , bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of\n            <jats:italic>integer-pointer casts<\/jats:italic>\n            . Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee. However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.\n          <\/jats:p>\n          <jats:p>In this paper, we introduce VIP, a new memory object model aimed at supporting C verification. VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI\u2019s validation with respect to practice. In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP\u2019s expressiveness via an implementation in the Cerberus C semantics.<\/jats:p>","DOI":"10.1145\/3498681","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["VIP: verifying real-world C idioms with integer-pointer casts"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2849-5338","authenticated-orcid":false,"given":"Rodolphe","family":"Lepigre","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3723-636X","authenticated-orcid":false,"given":"Kayvan","family":"Memarian","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9496-y"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"e_1_2_2_8_1","unstructured":"Jeffrey Cook and Sakthi Subramanian. 1994. A Formal Semantics for C in Nqthm. Trusted Information Systems.  Jeffrey Cook and Sakthi Subramanian. 1994. A Formal Semantics for C in Nqthm. Trusted Information Systems."},{"key":"e_1_2_2_9_1","unstructured":"Will Deacon. 2020. Virtualization for the Masses: Exposing KVM on Android. https:\/\/www.youtube.com\/watch?v=wY-u6n75iXc KVM Forum Talk.  Will Deacon. 2020. Virtualization for the Masses: Exposing KVM on Android. https:\/\/www.youtube.com\/watch?v=wY-u6n75iXc KVM Forum Talk."},{"key":"e_1_2_2_10_1","unstructured":"Jake Edge. 2020. KVM for Android. https:\/\/lwn.net\/Articles\/836693\/  Jake Edge. 2020. KVM for Android. https:\/\/lwn.net\/Articles\/836693\/"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56992-8_17"},{"key":"e_1_2_2_17_1","unstructured":"Jens Gustedt Peter Sewell Kayvan Memarian Victor B. F. Gomes and Martin Uecker. 2020. N2577: A Provenance-aware Memory Object Model for C. Working Draft Technical Specification TS 6010. ISO\/IEC JTC1\/SC22\/WG14 N2577. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n2577.pdf  Jens Gustedt Peter Sewell Kayvan Memarian Victor B. F. Gomes and Martin Uecker. 2020. N2577: A Provenance-aware Memory Object Model for C. Working Draft Technical Specification TS 6010. ISO\/IEC JTC1\/SC22\/WG14 N2577. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n2577.pdf"},{"key":"e_1_2_2_18_1","unstructured":"Hafnium. 2020. Hafnium. https:\/\/review.trustedfirmware.org\/plugins\/gitiles\/hafnium\/hafnium\/+\/HEAD\/README.md  Hafnium. 2020. Hafnium. https:\/\/review.trustedfirmware.org\/plugins\/gitiles\/hafnium\/hafnium\/+\/HEAD\/README.md"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5662349"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5662349"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_39_1","unstructured":"Xavier Leroy Andrew Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert memory model version 2. Inria.  Xavier Leroy Andrew Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert memory model version 2. Inria."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_41_1","unstructured":"Xavier Leroy and Damien Doligez. 1996. OCaml runtime representation of values. https:\/\/github.com\/ocaml\/ocaml\/blob\/trunk\/runtime\/caml\/mlvalues.h  Xavier Leroy and Damien Doligez. 1996. OCaml runtime representation of values. https:\/\/github.com\/ocaml\/ocaml\/blob\/trunk\/runtime\/caml\/mlvalues.h"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_49_1","unstructured":"pKVM developers. 2020. Initial allocator of the pKVM hypervisor. https:\/\/github.com\/torvalds\/linux\/blob\/master\/arch\/arm64\/kvm\/hyp\/nvhe\/early_alloc.c  pKVM developers. 2020. Initial allocator of the pKVM hypervisor. https:\/\/github.com\/torvalds\/linux\/blob\/master\/arch\/arm64\/kvm\/hyp\/nvhe\/early_alloc.c"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.05.010"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360597"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_2_2_59_1","unstructured":"WG14. 2004. Defect Report #260: Indeterminate values and identical representations. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm  WG14. 2004. Defect Report #260: Indeterminate values and identical representations. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498681","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498681","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498681"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498681"],"URL":"https:\/\/doi.org\/10.1145\/3498681","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}