{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T11:58:53Z","timestamp":1787313533008,"version":"3.56.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032071934","type":"print"},{"value":"9783032071941","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T00:00:00Z","timestamp":1760486400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T00:00:00Z","timestamp":1760486400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07194-1_4","type":"book-chapter","created":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T18:07:05Z","timestamp":1760465225000},"page":"54-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying MPI API Usage Requirements with\u00a0Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-9922-3112","authenticated-orcid":false,"given":"Yussur Mustafa","family":"Oraji","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7121-7205","authenticated-orcid":false,"given":"Simon","family":"Schwitanski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1931-773X","authenticated-orcid":false,"given":"Alexander","family":"H\u00fcck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0640-8966","authenticated-orcid":false,"given":"Joachim","family":"Jenke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1641-4342","authenticated-orcid":false,"given":"Sebastian","family":"Kreutzer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2711-3032","authenticated-orcid":false,"given":"Christian","family":"Bischof","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,15]]},"reference":[{"key":"4_CR1","unstructured":"Berne, J., Doumler, T., Krzemie\u0144ski, A.: Contracts for C++, https:\/\/www.openstd.org\/jtc1\/sc22\/wg21\/docs\/papers\/2025\/p2900r14.pdf (visited on 05\/13\/2025)"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors Tool Set: Verification of Parallel and Concurrent Software. In: Polikarpova, N., Schneider, S. (eds.) Integrated Formal Methods, pp. 102\u2013110. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Burak, S., Ivanov, I.R., Domke, J., M\u00fcller, M.: SPMD IR: Unifying SPMD and Multivalue IR Showcased for Static Verification of Collectives. In: Blaas-Schenner, C., Niethammer, C., Haas, T. (eds.) Recent Advances in the Message Passing Interface, pp. 3\u201320. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-73370-3_1","DOI":"10.1007\/978-3-031-73370-3_1"},{"issue":"1","key":"4_CR4","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/99.660313","volume":"5","author":"L Dagum","year":"1998","unstructured":"Dagum, L., Menon, R.: Openmp: an industry standard api for shared-memory programming. IEEE Comput. Sci. Eng. 5(1), 46\u201355 (1998). https:\/\/doi.org\/10.1109\/99.660313","journal-title":"IEEE Comput. Sci. Eng."},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Droste, A., Kuhn, M., Ludwig, T.: MPI-checker: Static Analysis for MPI. In: Proceedings of the Second Workshop on the LLVM Compiler Infrastructure in HPC. LLVM \u201915, pp. 1\u201310. Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2833157.2833159","DOI":"10.1145\/2833157.2833159"},{"key":"4_CR6","unstructured":"GASPI Forum, GASPI: Global Address Space Programming Interface 17.1, (2017). https:\/\/raw.githubusercontent.com\/GASPI-Forum\/GASPI-Forum.github.io\/master\/standards\/GASPI-17.1.pdf (visited on 12\/30\/2024)"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Ghosh, S., Halappanavar, M., Tumeo, A., Kalyanaraman, A., Gebremedhin, A.H.: MiniVite: A Graph Analytics Benchmarking Tool for Massively Parallel Systems. In: 2018 IEEE\/ACM Performance Modeling, Benchmarking and Simulation of High Performance Computer Systems (PMBS), pp. 51\u201356 (2018). https:\/\/doi.org\/10.1109\/PMBS.2018.8641631","DOI":"10.1109\/PMBS.2018.8641631"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Hilbrich, T., Schulz, M., de Supinski, B.R., M\u00fcller, M.S.: MUST: A Scalable Approach to Runtime Error Detection in MPI Programs. In: M\u00fcller, M.S., Resch, M.M., Schulz, A., Nagel, W.E. (eds.) Tools for High Performance Computing 2009, pp. 53\u201366. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11261-4_5","DOI":"10.1007\/978-3-642-11261-4_5"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Jammer, T., Saillard, E., Schwitanski, S., Jenke, J., Vinayagame, R., H\u00fcck, A., Bischof, C.: MPI-BugBench: A Framework for Assessing MPI Correctness Tools. In: Blaas-Schenner, C., Niethammer, C., Haas, T. (eds.) Recent Advances in the Message Passing Interface, pp. 121\u2013137. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-73370-3_8","DOI":"10.1007\/978-3-031-73370-3_8"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Karlin, I., Keasler, J., Neely, J.: LULESH 2.0 Updates and Changes. LLNL-TR-641973, 1090032, LLNL-TR\u2013641973, 1090032 (2013). https:\/\/doi.org\/10.2172\/1090032","DOI":"10.2172\/1090032"},{"key":"4_CR11","unstructured":"Kotlin Contracts Proposal, GitHub. (2019). https:\/\/github.com\/Kotlin\/KEEP\/blob\/master\/proposals\/kotlin-contracts.md (visited on 02\/07\/2025)"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: International Symposium on Code Generation and Optimization, 2004. CGO 2004. Pp. 75\u201386 (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"4_CR13","unstructured":"L\u00fchrs, S.: Automated Benchmarking with JUBE. FZJ-2020-02622, J\u00fclich Supercomputing Center (2020). https:\/\/juser.fz-juelich.de\/record\/878080 (visited on 10\/28\/2024)"},{"key":"4_CR14","unstructured":"Message Passing Interface Forum, MPI: A Message-Passing Interface Standard Version 4.1, (2023). https:\/\/www.mpi-forum.org\/docs\/mpi-4.1\/mpi41-report.pdf"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin, Heidelberg (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"4_CR16","unstructured":"OpenSHMEM Committee, OpenSHMEM: Application Programming Interface Version 1.5, (2020). http:\/\/openshmem.org\/site\/sites\/default\/site_files\/OpenSHMEM-1.5.pdf (visited on 12\/30\/2024)"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Oraji, Y.M.: Artifact for \u2019Verifying MPI API Usage Requirements with Contracts\u2019. https:\/\/doi.org\/10.5281\/zenodo.15574135","DOI":"10.5281\/zenodo.15574135"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Parr, T.J., Quong, R.W.: ANTLR: A Predicated-LL(k) Parser Generator. Software: Practice and Experience 25(7), 789\u2013810 (1995). https:\/\/doi.org\/10.1002\/spe.4380250705","DOI":"10.1002\/spe.4380250705"},{"issue":"4","key":"4_CR19","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1177\/1094342014552204","volume":"28","author":"E Saillard","year":"2014","unstructured":"Saillard, E., Carribault, P., Barthou, D.: Parcoach: combining static and dynamic validation of mpi collective communications. The International Journal of High Performance Computing Applications 28(4), 425\u2013434 (2014). https:\/\/doi.org\/10.1177\/1094342014552204","journal-title":"The International Journal of High Performance Computing Applications"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Saillard, E., Sergent, M., Ait Kaci, C.T., Barthou, D.: Static Local Concurrency Errors Detection in MPI-RMA Programs. In: 2022 IEEE\/ACM Sixth International Workshop on Software Correctness for HPC Applications (Correctness), pp. 18\u201326 (2022). https:\/\/doi.org\/10.1109\/Correctness56720.2022.00008","DOI":"10.1109\/Correctness56720.2022.00008"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Schwitanski, S., Jenke, J., Klotz, S., M\u00fcller, M.S.: RMARaceBench: A Microbenchmark Suite to Evaluate Race Detection Tools for RMA Programs. In: Proceedings of the SC \u201923 Workshops of The International Conference on High Performance Computing, Network, Storage, and Analysis. SC-W \u201923, pp. 205\u2013214. Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3624062.3624087","DOI":"10.1145\/3624062.3624087"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Schwitanski, S., Oraji, Y.M., P\u00e4tzold, C., Jenke, J., M\u00fcller, M.S.: Leveraging Static Analysis to Accelerate Dynamic Race Detection for Remote Memory Access Programs. In: Weiland, M., Neuwirth, S., Kruse, C., Weinzierl, T. (eds.) High Performance Computing. ISC High Performance 2024 International Workshops, pp. 45\u201358. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-73716-9_4","DOI":"10.1007\/978-3-031-73716-9_4"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Schwitanski, S., Oraji, Y.M., P\u00e4tzold, C., Jenke, J., Tomski, F., M\u00fcller, M.S.: RMASanitizer: Generalized Runtime Detection of Data Races in Remote Memory Access Applications. In: Proceedings of the 53rd International Conference on Parallel Processing. ICPP \u201924, pp. 833\u2013844. Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3673038.3673109","DOI":"10.1145\/3673038.3673109"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Van der Wijngaart, R.F., Mattson, T.G.: The Parallel Research Kernels. In: 2014 IEEE High Performance Extreme Computing Conference (HPEC), pp. 1\u20136 (2014). https:\/\/doi.org\/10.1109\/HPEC.2014.7040972","DOI":"10.1109\/HPEC.2014.7040972"}],"container-title":["Lecture Notes in Computer Science","Recent Advances in the Message Passing Interface"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07194-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T10:53:54Z","timestamp":1774954434000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07194-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,15]]},"ISBN":["9783032071934","9783032071941"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07194-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,15]]},"assertion":[{"value":"15 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}