{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:47:51Z","timestamp":1767926871255,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100012693","name":"Yale-NUS College","doi-asserted-by":"publisher","award":["R-607-265-322-121"],"award-info":[{"award-number":["R-607-265-322-121"]}],"id":[{"id":"10.13039\/100012693","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Shanghai Pujiang Program","award":["19PJ1406000"],"award-info":[{"award-number":["19PJ1406000"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1521602"],"award-info":[{"award-number":["CCF-1521602"]}],"id":[{"id":"10.13039\/100000001","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":[[2019,10,10]]},"abstract":"<jats:p>We develop powerful and general techniques to mechanically verify realistic programs that manipulate heap-represented graphs. These graphs can exhibit well-known organization principles, such as being a directed acyclic graph or a disjoint-forest; alternatively, these graphs can be totally unstructured. The common thread for such structures is that they exhibit deep intrinsic sharing and can be expressed using the language of graph theory. We construct a modular and general setup for reasoning about abstract mathematical graphs and use separation logic to define how such abstract graphs are represented concretely in the heap. We develop a Localize rule that enables modular reasoning about such programs, and show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. We demonstrate the generality and power of our techniques by integrating them into the Verified Software Toolchain and certifying the correctness of seven graph-manipulating programs written in CompCert C, including a 400-line generational garbage collector for the CertiCoq project. While doing so, we identify two places where the semantics of C is too weak to define generational garbage collectors of the sort used in the OCaml runtime. Our proofs are entirely machine-checked in Coq.<\/jats:p>","DOI":"10.1145\/3360597","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Certifying graph-manipulating C programs via localizations within data structures"],"prefix":"10.1145","volume":"3","author":[{"given":"Shengyi","family":"Wang","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}]},{"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}]},{"given":"Anshuman","family":"Mohan","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"The Third International Workshop on Coq for Programming Languages (CoqPL).","author":"Anand Abhishek","year":"2017"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_2_2_3_1","volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W."},{"key":"e_1_2_2_4_1","volume-title":"Appel and David McAllester","author":"Andrew","year":"2001"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_6"},{"key":"e_1_2_2_7_1","volume-title":"Schmitt","author":"Beckert Bernhard","year":"2007"},{"key":"e_1_2_2_8_1","volume-title":"Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. 315\u2013331","author":"Bengtson Jesper","year":"2012"},{"key":"e_1_2_2_9_1","volume-title":"O\u2019Hearn","author":"Berdine Josh","year":"2005"},{"key":"e_1_2_2_10_1","volume-title":"SPACE","volume":"4","author":"Bornat R."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.059"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863590"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_2_2_16_1","volume-title":"Formal Proofs of Tarjan\u2019s Algorithm in Why3, Coq, and Isabelle. CoRR abs\/1810.11979","author":"Chen Ran","year":"2018"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/362790.362798"},{"key":"e_1_2_2_18_1","volume-title":"Huu Hai Nguyen, and Shengchao Qin","author":"Chin Wei Ngan","year":"2010"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_2_20_1","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"Chou Ching-Tsun"},{"key":"e_1_2_2_21_1","volume-title":"Stein","author":"Cormen Thomas H.","year":"2009","edition":"3"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_2_24_1","volume-title":"7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings. 161\u2013177","author":"Dockins Robert"},{"key":"e_1_2_2_25_1","volume-title":"Vingt-sixi\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA","author":"Dubois Catherine","year":"2015"},{"key":"e_1_2_2_26_1","volume-title":"A Coq toolkit for graph theory. Rapport de recherche 15","author":"Duprat Jean","year":"2001"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_28"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738006"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_2_2_30_1","unstructured":"Georges Gonthier. 2005. A computer-checked proof of the four colour theorem.  Georges Gonthier. 2005. A computer-checked proof of the four colour theorem."},{"key":"e_1_2_2_31_1","volume-title":"ITP 2019, Portland, USA, September 8-13, 2019, Proceedings.","author":"Gu\u00e9neau Arma\u00ebl","year":"2019"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"e_1_2_2_33_1","unstructured":"Jason Hickey Anil Madhavapeddy and Yaron Minsky. 2014. Real World OCaml. OReilly.  Jason Hickey Anil Madhavapeddy and Yaron Minsky. 2014. Real World OCaml. OReilly."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693165"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9442-4"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863584"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250788"},{"key":"e_1_2_2_45_1","volume-title":"1st International Conference on Formal Structures for Computation and Deduction (FSCD","author":"Nipkow Tobias","year":"2016"},{"key":"e_1_2_2_46_1","volume-title":"Dijkstra\u2019s Shortest Path Algorithm. Archive of Formal Proofs (Jan","author":"Nordhoff Benedikt","year":"2012"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0183-z"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","volume-title":"Local Reasoning about Programs that Alter Data Structures","author":"O\u2019Hearn Peter","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_50_1","first-page":"286","article-title":"A Primer on Separation Logic (and Automatic Program Verification and Analysis)","volume":"33","author":"O\u2019Hearn Peter W.","year":"2012","journal-title":"Software Safety and Security"},{"key":"e_1_2_2_51_1","volume-title":"Automated Verification of Practical Garbage Collectors. Logical Methods in Computer Science 6","author":"Petrank Erez","year":"2010"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806615"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_2_54_1","unstructured":"John C. Reynolds. 2003. A Short Course on Separation Logic. (2003). http:\/\/www.cs.cmu.edu\/afs\/cs.cmu.edu\/project\/fox19\/member\/jcr\/wwwaac2003\/notes7.ps .  John C. Reynolds. 2003. A Short Course on Separation Logic. (2003). http:\/\/www.cs.cmu.edu\/afs\/cs.cmu.edu\/project\/fox19\/member\/jcr\/wwwaac2003\/notes7.ps ."},{"key":"e_1_2_2_55_1","unstructured":"Tom Ridge. 2005. Graphs and Trees in Isabelle\/HOL. (2005).  Tom Ridge. 2005. Graphs and Trees in Isabelle\/HOL. (2005)."},{"key":"e_1_2_2_56_1","doi-asserted-by":"crossref","unstructured":"Ilya Sergey Aleksandar Nanevski and Anindya Banerjee. 2015. Mechanized Verification of Fine-grained Concurrent Programs. In PLDI. 77\u201387.  Ilya Sergey Aleksandar Nanevski and Anindya Banerjee. 2015. Mechanized Verification of Fine-grained Concurrent Programs. In PLDI. 77\u201387.","DOI":"10.1145\/2813885.2737964"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.2000.873806"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_2_59_1","unstructured":"Shengyi Wang Qinxiang Cao Anshuman Mohan and Aquinas Hobor. 2019. Extended Autoquack. https:\/\/www.comp.nus. edu.sg\/~hobor\/Publications\/2019\/autoquack_extended_oopsla19.pdf  Shengyi Wang Qinxiang Cao Anshuman Mohan and Aquinas Hobor. 2019. Extended Autoquack. https:\/\/www.comp.nus. edu.sg\/~hobor\/Publications\/2019\/autoquack_extended_oopsla19.pdf"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/HOL.1991.596304"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60275-5_77"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055153"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360597","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360597","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360597","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":59,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360597"],"URL":"https:\/\/doi.org\/10.1145\/3360597","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}