{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T23:42:17Z","timestamp":1783035737105,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T00:00:00Z","timestamp":1740441600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["2234376"],"award-info":[{"award-number":["2234376"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,2,25]]},"DOI":"10.1145\/3708493.3712690","type":"proceedings-article","created":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T17:02:04Z","timestamp":1740502924000},"page":"128-140","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Scalable Data-Flow Modeling and Validation of Distributed-Memory Algorithms"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-6599-565X","authenticated-orcid":false,"given":"Raneem","family":"Abu-Yosef","sequence":"first","affiliation":[{"name":"The Ohio State University, Columbus, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8008-0220","authenticated-orcid":false,"given":"Martin","family":"Kong","sequence":"additional","affiliation":[{"name":"The Ohio State University, Columbus, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,2,25]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447818.3460369"},{"key":"e_1_3_2_1_2_1","unstructured":"Raneem Abu-Yosef and Martin Kong. 2025. Scalable Data-Flow Modeling and Validation of Distributed-Memory Algorithms (GitHub). https:\/\/github.com\/raneemabuyosef\/collectCall\/"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.1553"},{"key":"e_1_3_2_1_4_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT press, USA."},{"key":"e_1_3_2_1_5_1","unstructured":"C\u00e9dric BASTOUL. 2012. TH\u00c8SE DE L\u2019UNIVERSIT\u00c9 PARIS-SUD. Ph. D. Dissertation. INRIA Saclay. http:\/\/icps.u-strasbg.fr\/people\/bastoul\/public_html\/research\/papers\/Bastoul_HDR.pdf"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503210.2503289"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.32"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966463"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, USA. 209\u2013224."},{"key":"e_1_3_2_1_10_1","volume-title":"A cellular computer to implement the Kalman filter algorithm","author":"Cannon Lynn Elliot","unstructured":"Lynn Elliot Cannon. 1969. A cellular computer to implement the Kalman filter algorithm. Montana State University, USA."},{"key":"e_1_3_2_1_11_1","unstructured":"Ohio Supercomputer Center. 1987. Ohio Supercomputer Center. http:\/\/osc.edu\/ark:\/19495\/f5s1ph73"},{"key":"e_1_3_2_1_12_1","unstructured":"Ohio Supercomputer Center. 2018. Pitzer Supercomputer. http:\/\/osc.edu\/ark:\/19495\/hpc56htp"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2012.127"},{"key":"e_1_3_2_1_14_1","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke. 1997. Model checking. In Foundations of Software Technology and Theoretical Computer Science, S. Ramesh and G. Sivakumar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 54\u201356. isbn:978-3-540-69659-9"},{"key":"e_1_3_2_1_15_1","volume-title":"Analysis of protein circular dichroism spectra for secondary structure using a simple matrix multiplication. Analytical biochemistry, 155, 1","author":"Compton Larry A","year":"1986","unstructured":"Larry A Compton and W Curtis Johnson Jr. 1986. Analysis of protein circular dichroism spectra for secondary structure using a simple matrix multiplication. Analytical biochemistry, 155, 1 (1986), 155\u2013167."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_17_1","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2022. Z3 Prover. https:\/\/github.com\/Z3Prover\/z3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2833157.2833159"},{"key":"e_1_3_2_1_19_1","volume-title":"MPI-checker: static analysis for MPI. https:\/\/github.com\/0ax1\/MPI-Checker Accessed","author":"Droste Alexander","year":"2024","unstructured":"Alexander Droste, Michael Kuhn, and Thomas Ludwig. 2015. MPI-checker: static analysis for MPI. https:\/\/github.com\/0ax1\/MPI-Checker Accessed September 2024"},{"key":"e_1_3_2_1_20_1","volume-title":"Using MPI: portable parallel programming with the message-passing interface. 1","author":"Gropp William","unstructured":"William Gropp, Ewing Lusk, and Anthony Skjellum. 1999. Using MPI: portable parallel programming with the message-passing interface. 1, MIT press, USA."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/155332.155349"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542275.1542319"},{"key":"e_1_3_2_1_23_1","volume-title":"Intel Thread Analyzer and Collector. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/oneapi\/trace-analyzer.html Accessed on","year":"2024","unstructured":"Intel. 2022. Intel Thread Analyzer and Collector. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/oneapi\/trace-analyzer.html Accessed on October 2024"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO57630.2024.10444795"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3581784.3607096"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127024.3127032"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201907)","author":"Palmer Robert","unstructured":"Robert Palmer, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby. 2007. An approach to formalization and analysis of message passing libraries. In Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201907). Springer-Verlag, Berlin, Heidelberg. 164\u2013181. isbn:3540797068"},{"key":"e_1_3_2_1_29_1","volume-title":"2000 IEEE International Symposium on Performance Analysis of Systems and Software. ISPASS (Cat. No. 00EX422)","author":"Sarkar Vivek","year":"2000","unstructured":"Vivek Sarkar and Nimrod Megiddo. 2000. An analytical model for loop tiling and its solution. In 2000 IEEE International Symposium on Performance Analysis of Systems and Software. ISPASS (Cat. No. 00EX422). 146\u2013153."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87475-1_36"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1177\/1094342006064482"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941603"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.2006.32"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30218-6_11"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9128(199704)9:4<255::AID-CPE250>3.0.CO;2-2"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15582-6_49"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-006-1231-0"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504214"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2018.00066"},{"key":"e_1_3_2_1_41_1","unstructured":"Fangke Ye Jisheng Zhao and Vivek Sarkar. 2019. Detecting MPI usage anomalies via partial program symbolic execution (Artifact). https:\/\/github.com\/fkye\/PSE-MPI"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380419"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.99"}],"event":{"name":"CC '25: 34th ACM SIGPLAN International Conference on Compiler Construction","location":"Las Vegas NV USA","acronym":"CC '25","sponsor":["SIGPLAN SIGPLAN Programming Languages"]},"container-title":["Proceedings of the 34th ACM SIGPLAN International Conference on Compiler Construction"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708493.3712690","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3708493.3712690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:09:54Z","timestamp":1750295394000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708493.3712690"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,25]]},"references-count":44,"alternative-id":["10.1145\/3708493.3712690","10.1145\/3708493"],"URL":"https:\/\/doi.org\/10.1145\/3708493.3712690","relation":{},"subject":[],"published":{"date-parts":[[2025,2,25]]},"assertion":[{"value":"2025-02-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}