{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:21Z","timestamp":1767929541151,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001459","name":"Singapore Ministry of Education","doi-asserted-by":"crossref","award":["MOE-MOET32021-0001"],"award-info":[{"award-number":["MOE-MOET32021-0001"]}],"id":[{"id":"10.13039\/501100001459","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,6,20]]},"abstract":"<jats:p>\n            Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit\n            <jats:italic toggle=\"yes\">structural properties<\/jats:italic>\n            of the data stored in an array (\n            <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n            ., repetition or sparsity) to develop a specialised representation optimised for space efficiency. Formally reasoning about correctness of manipulations with such structured data is challenging, as they are often composed of multiple loops with non-trivial invariants.\n          <\/jats:p>\n          <jats:p>\n            In this work, we observe that specifications for structured data manipulations can be phrased as\n            <jats:italic toggle=\"yes\">hypersafety<\/jats:italic>\n            properties,\n            <jats:italic toggle=\"yes\">i.e<\/jats:italic>\n            ., predicates that relate traces of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>k<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            programs. To turn this observation into an effective verification methodology, we developed the Logic for Graceful Tensor Manipulation (LGTM), a new Hoare-style relational separation logic for specifying and verifying computations over structured data. The key enabling idea of LGTM is that of\n            <jats:italic toggle=\"yes\">parametrised<\/jats:italic>\n            hypersafety specifications that allow the number\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>k<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            of the program components to depend on the\n            <jats:italic toggle=\"yes\">program variables<\/jats:italic>\n            . We implemented LGTM as a foundational embedding into Coq, mechanising its rules, meta-theory, and the proof of soundness. Furthermore, we developed a library of domain-specific tactics that automate computer-aided hypersafety reasoning, resulting in pleasantly short proof scripts that enjoy a high degree of reuse. We argue for the effectiveness of relational reasoning about structured data in LGTM by specifying and mechanically proving correctness of 13 case studies including computations on compressed arrays and efficient operations over multiple kinds of sparse tensors.\n          <\/jats:p>","DOI":"10.1145\/3656403","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"647-670","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Mechanised Hypersafety Proofs about Structured Data"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9233-3133","authenticated-orcid":false,"given":"Vladimir","family":"Gladshtein","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1017-1562","authenticated-orcid":false,"given":"Qiyuan","family":"Zhao","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4963-0869","authenticated-orcid":false,"given":"Willow","family":"Ahrens","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7231-7643","authenticated-orcid":false,"given":"Saman","family":"Amarasinghe","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Willow Ahrens Daniel Donenfeld Fredrik Kjolstad and Saman P. Amarasinghe. 2023. Looplets: A Language for Structured Coiteration. In CGO. ACM 41\u201354. https:\/\/doi.org\/10.1145\/3579990.3580020 10.1145\/3579990.3580020","DOI":"10.1145\/3579990.3580020"},{"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","unstructured":"Andrew W. Appel. 2022. Coq\u2019s vibrant ecosystem for verification engineering (invited talk). In CPP. ACM 2\u201311. https:\/\/doi.org\/10.1145\/3497775.3503951 10.1145\/3497775.3503951","DOI":"10.1145\/3497775.3503951"},{"key":"e_1_3_1_5_1","volume-title":"Ph. D. Dissertation","author":"Arnold Gilad","year":"2011","unstructured":"Gilad Arnold. 2011. Data-Parallel Language for Correct and Efficient Sparse Matrix Codes. Ph. D. Dissertation. University of California, Berkeley, USA. http:\/\/www.escholarship.org\/uc\/item\/2pw6165p"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Gilad Arnold Johannes H\u00f6lzl Ali Sinan K\u00f6ksal Rastislav Bod\u00edk and Mooly Sagiv. 2010. Specifying and verifying sparse matrix codes. In ICFP. ACM 249\u2013260. https:\/\/doi.org\/10.1145\/1863543.1863581 10.1145\/1863543.1863581","DOI":"10.1145\/1863543.1863581"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Boris K\u00f6pf Federico Olmedo and Santiago Zanella B\u00e9guelin. 2012. Probabilistic relational reasoning for differential privacy. In POPL. ACM 97\u2013110. https:\/\/doi.org\/10.1145\/2103656.2103670 10.1145\/2103656.2103670","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In POPL. ACM 14\u201325. https:\/\/doi.org\/10.1145\/964001.964003 10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Michael Carbin Deokhwan Kim Sasa Misailovic and Martin C. Rinard. 2012. Proving acceptability properties of relaxed nondeterministic approximate programs. In PLDI. ACM 169\u2013180. https:\/\/doi.org\/10.1145\/2254064.2254086 10.1145\/2254064.2254086","DOI":"10.1145\/2254064.2254086"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Arthur Chargu\u00e9raud. 2011. Characteristic Formulae for the Verification of Imperative Programs. In ICFP. ACM 418\u2013430. https:\/\/doi.org\/10.1145\/2034773.2034828 10.1145\/2034773.2034828","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563338"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276493"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Stephen Chou Fredrik Kjolstad and Saman P. Amarasinghe. 2020. Automatic generation of efficient sparse tensor format conversion routines. In PLDI. ACM 823\u2013838. https:\/\/doi.org\/10.1145\/3385412.3385963 10.1145\/3385412.3385963","DOI":"10.1145\/3385412.3385963"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Daniel Donenfeld Stephen Chou and Saman P. Amarasinghe. 2022. Unified Compilation for Lossless Compression and Sparse Computing. In CGO. IEEE 205\u2013216. https:\/\/doi.org\/10.1109\/CGO53902.2022.9741282 10.1109\/CGO53902.2022.9741282","DOI":"10.1109\/CGO53902.2022.9741282"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563298"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/Correctness49594.2019.00010"},{"key":"e_1_3_1_20_1","unstructured":"Pratik Fegade Tianqi Chen Phillip B. Gibbons and Todd C. Mowry. 2022. The CoRa Tensor Compiler: Compilation for Ragged Tensors with Minimal Padding. In MLSys.mlsys.org. https:\/\/proceedings.mlsys.org\/paper\/2022\/hash\/d3d9446802a44259755d38e6d163e820-Abstract.html"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Vladimir Gladshtein Qiyuan Zhao Willow Ahrens Saman Amarasinghe and Ilya Sergey. 2024a. LGTM: the Logic for Graceful Tensor Manipulation. https:\/\/doi.org\/10.5281\/zenodo.10951930 10.5281\/zenodo.10951930","DOI":"10.5281\/zenodo.10951930"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Vladimir Gladshtein Qiyuan Zhao Willow Ahrens Saman Amarasinghe and Ilya Sergey. 2024b. Mechanised Hypersafety Proofs about Structured Data: Extended Version. CoRR abs\/2404.06477 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2404.06477 10.48550\/ARXIV.2404.06477","DOI":"10.48550\/ARXIV.2404.06477"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Changwan Hong Aravind Sukumaran Rajam Israt Nisa Kunal Singh and Ponnuswamy Sadayappan. 2019. Adaptive sparse tiling for sparse matrix multiplication. In PPoPP. ACM 300\u2013314. https:\/\/doi.org\/10.1145\/3293883.3295712 10.1145\/3293883.3295712","DOI":"10.1145\/3293883.3295712"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH58626.2023.00021"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Oleg Kiselyov Aggelos Biboudis Nick Palladinos and Yannis Smaragdakis. 2017. Stream fusion to completeness. In POPL. ACM 285\u2013299. https:\/\/doi.org\/10.1145\/3009837.3009880 10.1145\/3009837.3009880","DOI":"10.1145\/3009837.3009880"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Fredrik Kjolstad Willow Ahrens Shoaib Kamil and Saman Amarasinghe. 2019. Tensor Algebra Compilation with Workspaces. In CGO. 180\u2013192. https:\/\/doi.org\/10.1109\/CGO.2019.8661185 10.1109\/CGO.2019.8661185","DOI":"10.1109\/CGO.2019.8661185"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133901"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591268"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498717"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. https:\/\/doi.org\/10.5281\/zenodo.7118596 10.5281\/zenodo.7118596","DOI":"10.5281\/zenodo.7118596"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.12"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Tobi Popoola Tuowen Zhao Aaron St. George Kalyan Bhetwal Michelle Mills Strout Mary Hall and Catherine Olschanowsky. 2023. Code Synthesis for Sparse Tensor Format Conversion and Optimization. In CGO. ACM 28\u201340. https:\/\/doi.org\/10.1145\/3579990.3580021 10.1145\/3579990.3580021","DOI":"10.1145\/3579990.3580021"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133900"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare Logic for Verifying k-Safety Properties. In PLDI. ACM 57\u201369. https:\/\/doi.org\/10.1145\/2908080.2908092 10.1145\/2908080.2908092","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473589"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Zihao Ye Ruihang Lai Junru Shao Tianqi Chen and Luis Ceze. 2023. SparseTIR: Composable Abstractions for Sparse Compilation in Deep Learning. In ASPLOS. ACM 660\u2013678. https:\/\/doi.org\/10.1145\/3582016.3582047 10.1145\/3582016.3582047","DOI":"10.1145\/3582016.3582047"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656403","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:40:22Z","timestamp":1751661622000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":37,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656403"],"URL":"https:\/\/doi.org\/10.1145\/3656403","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}