{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:04Z","timestamp":1750221304368,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006168","name":"National Nuclear Security Administration","doi-asserted-by":"publisher","award":["DE-NA0002373-1"],"award-info":[{"award-number":["DE-NA0002373-1"]}],"id":[{"id":"10.13039\/100006168","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1160904"],"award-info":[{"award-number":["CCF-1160904"]}],"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":[[2017,10,12]]},"abstract":"<jats:p>Algorithms that create and mutate graph data structures are challenging to implement correctly. However, verifying even basic properties of low-level implementations, such as referential integrity and memory safety, remains non-trivial. Furthermore, any extension to such a data structure multiplies the complexity of its implementation, while compounding the challenges in reasoning about correctness. We take a language design approach to this problem. We propose Seam, a language for expressing local edits to graph-like data structures, based on a relational data model, and such that data integrity can be verified automatically. We present a verification method that leverages an SMT solver, and prove it sound and precise (complete modulo termination of the SMT solver). We evaluate the verification capabilities of Seam empirically, and demonstrate its applicability to a variety of examples, most notably a new class of verification tasks derived from geometric remeshing operations used in scientific simulation and computer graphics. We describe our prototype implementation of a Seam compiler that generates low-level code, which can then be integrated into larger applications. We evaluate our compiler on a sample application, and demonstrate competitive execution time, compared to hand-written implementations.<\/jats:p>","DOI":"10.1145\/3133902","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Seam: provably safe local edits on graphs"],"prefix":"10.1145","volume":"1","author":[{"given":"Manolis","family":"Papadakis","sequence":"first","affiliation":[{"name":"Stanford University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilbert Louis","family":"Bernstein","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Sharma","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pat","family":"Hanrahan","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22655-7_23"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/237661.237692"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461912.2462027"},{"key":"e_1_2_2_5_1","volume-title":"Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohou\u00e9","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Catalin Hritcu , Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Peng Wang , Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohou\u00e9 . 2017 . Verified Low-Level Programming Embedded in F*. CoRR abs\/1703.00053 (2017). Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Catalin Hritcu, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohou\u00e9. 2017. Verified Low-Level Programming Embedded in F*. CoRR abs\/1703.00053 (2017)."},{"volume-title":"The Classical Decision Problem","author":"B\u00f6rger Egon","key":"e_1_2_2_6_1","unstructured":"Egon B\u00f6rger , Erich Gr\u00e4del , and Yuri Gurevich . 2001. The Classical Decision Problem . Springer Science & amp; Business Media. Egon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. 2001. The Classical Decision Problem. Springer Science &amp; Business Media."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/080737617"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480917"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45253-2_15"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601097.2601146"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987586"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462166"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993504"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254114"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199606)26:6%3C635::AID-SPE26%3E3.0.CO;2-P"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958053"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_2"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75103-8_1"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807085.1807100"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328461"},{"volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","key":"e_1_2_2_23_1","unstructured":"Leslie Lamport . 2002. Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/237218.237344"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461912.2462010"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2366145.2366171"},{"key":"e_1_2_2_32_1","volume-title":"Ccured: Type-Safe Retrofitting of Legacy Code. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Necula George C.","year":"2002","unstructured":"George C. Necula , Scott McPeak , and Westley Weimer . 2002 . Ccured: Type-Safe Retrofitting of Legacy Code. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages , Portland, OR, USA , January 16-18, 2002. 128\u2013139. George C. Necula, Scott McPeak, and Westley Weimer. 2002. Ccured: Type-Safe Retrofitting of Legacy Code. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002. 128\u2013139."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601097.2601132"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958054"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"e_1_2_2_37_1","unstructured":"J.-R. Sack and J. Urrutia (Eds.). 2000. Handbook of Computational Geometry. North-Holland Publishing Co. Amsterdam The Netherlands.  J.-R. Sack and J. Urrutia (Eds.). 2000. Handbook of Computational Geometry. North-Holland Publishing Co. Amsterdam The Netherlands."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908083"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_2_41_1","volume-title":"International Symposium on Applications of Graph Transformations with Industrial Relevance. Springer, 169\u2013181","author":"Strecker Martin","year":"2011","unstructured":"Martin Strecker . 2011 . Locality in Reasoning about Graph Transformations . In International Symposium on Applications of Graph Transformations with Industrial Relevance. Springer, 169\u2013181 . Martin Strecker. 2011. Locality in Reasoning about Graph Transformations. In International Symposium on Applications of Graph Transformations with Industrial Relevance. Springer, 169\u2013181."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984016"},{"key":"e_1_2_2_43_1","volume-title":"Widom","author":"Ullman Jeffrey D.","year":"2002","unstructured":"Jeffrey D. Ullman , Hector Garcia-Molina , and Jennifer D . Widom . 2002 . Database Systems : The Complete Book. Prentice Hall , Chapter 7. Jeffrey D. Ullman, Hector Garcia-Molina, and Jennifer D. Widom. 2002. Database Systems: The Complete Book. Prentice Hall, Chapter 7."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00185-2"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1531326.1531382"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1778765.1778787"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133902","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133902","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133902","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:25Z","timestamp":1750212805000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":46,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133902"],"URL":"https:\/\/doi.org\/10.1145\/3133902","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}