{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T09:06:00Z","timestamp":1781341560695,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T00:00:00Z","timestamp":1506297600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,9,25]]},"DOI":"10.1145\/3127024.3127032","type":"proceedings-article","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T11:58:11Z","timestamp":1503575891000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Verification of MPI programs using CIVL"],"prefix":"10.1145","author":[{"given":"Ziqing","family":"Luo","sequence":"first","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manchun","family":"Zheng","sequence":"additional","affiliation":[{"name":"Pure Storage Company"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen F.","family":"Siegel","sequence":"additional","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,9,25]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2464996.2467286"},{"key":"e_1_3_2_1_2_1","volume-title":"Lawrence Livermore National Laboratory Message-Passing Interface (MPI) Exercise. https:\/\/computing.llnl.gov\/tutorials\/mpi\/exercise.html. (2017). Accessed","author":"Barney Blaise","year":"2017","unstructured":"Blaise Barney . 2017. Lawrence Livermore National Laboratory Message-Passing Interface (MPI) Exercise. https:\/\/computing.llnl.gov\/tutorials\/mpi\/exercise.html. (2017). Accessed Aug. 5, 2017 . Blaise Barney. 2017. Lawrence Livermore National Laboratory Message-Passing Interface (MPI) Exercise. https:\/\/computing.llnl.gov\/tutorials\/mpi\/exercise.html. (2017). Accessed Aug. 5, 2017."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.32"},{"key":"e_1_3_2_1_4_1","volume-title":"Model checking","author":"Clarke Edmund M","unstructured":"Edmund M Clarke , Orna Grumberg , and Doron Peled . 1999. Model checking . MIT press , Cambridge, MA, USA . Edmund M Clarke, Orna Grumberg, and Doron Peled. 1999. Model checking. MIT press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_19"},{"key":"e_1_3_2_1_6_1","volume-title":"Using MPI: Portable Parallel Programming with the Message-Passing Interface","author":"Gropp Willaim","unstructured":"Willaim Gropp , Ewing Lusk , and Anthony Skjellum . 1999. Using MPI: Portable Parallel Programming with the Message-Passing Interface . MIT Press , Cambridge, MA . Willaim Gropp, Ewing Lusk, and Anthony Skjellum. 1999. Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge, MA."},{"key":"e_1_3_2_1_7_1","volume-title":"M\u00fcller","author":"Hilbrich Tobias","year":"2012","unstructured":"Tobias Hilbrich , Joachim Protze , Martin Schulz , Bronis R. de Supinski , and Matthias S . M\u00fcller . 2012 . MPI Runtime Error Detection with MUST : Advances in Deadlock Detection. In International Conference on High Performance Computing Networking, Storage and Analysis, SC '12, Salt Lake City, UT, USA - November 11--15, 2012, Jeffrey K. Hollingsworth (Ed.). IEEE Computer Society Press , Los Alamitos, CA, USA, Article 30, 11 pages. http:\/\/dl.acm.org\/citation.cfm?id=2388996.2389037 Tobias Hilbrich, Joachim Protze, Martin Schulz, Bronis R. de Supinski, and Matthias S. M\u00fcller. 2012. MPI Runtime Error Detection with MUST: Advances in Deadlock Detection. In International Conference on High Performance Computing Networking, Storage and Analysis, SC '12, Salt Lake City, UT, USA - November 11--15, 2012, Jeffrey K. Hollingsworth (Ed.). IEEE Computer Society Press, Los Alamitos, CA, USA, Article 30, 11 pages. http:\/\/dl.acm.org\/citation.cfm?id=2388996.2389037"},{"key":"e_1_3_2_1_8_1","unstructured":"International Organization for Standardization and International Electrotechnical Commission. 2011. ISO\/IEC 989:2011 N1570: Programming Languages -- C. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1570.pdf. (12 April 2011).  International Organization for Standardization and International Electrotechnical Commission. 2011. ISO\/IEC 989:2011 N1570: Programming Languages -- C. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1570.pdf. (12 April 2011)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2523721.2523727"},{"key":"e_1_3_2_1_10_1","volume-title":"Euro-Par 2013: Parallel Processing Workshops","author":"Jordan Herbert","year":"2013","unstructured":"Herbert Jordan , Peter Thoman , and Thomas Fahringer . 2014. A High-Level IR Transformation System . In Euro-Par 2013: Parallel Processing Workshops , Aachen, Germany , August 26--27, 2013 . Revised Selected Papers (Lecture Notes in Computer Science), Vol. 8374 . Springer , Berlin, Heidelberg, 647--656. Herbert Jordan, Peter Thoman, and Thomas Fahringer. 2014. A High-Level IR Transformation System. In Euro-Par 2013: Parallel Processing Workshops, Aachen, Germany, August 26--27, 2013. Revised Selected Papers (Lecture Notes in Computer Science), Vol. 8374. Springer, Berlin, Heidelberg, 647--656."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814302"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.137.9"},{"key":"e_1_3_2_1_13_1","volume-title":"SPINning Parallel Systems Software. In Model Checking of Software: 9th Intl. SPIN Workshop (LNCS), Dragan Bosnacki and Stefan Leue (Eds.)","volume":"2318","author":"Matlin Olga Shumsky","year":"2002","unstructured":"Olga Shumsky Matlin , Ewing Lusk , and William McCune . 2002 . SPINning Parallel Systems Software. In Model Checking of Software: 9th Intl. SPIN Workshop (LNCS), Dragan Bosnacki and Stefan Leue (Eds.) , Vol. 2318 . Springer, Berlin, Heidelberg, 213--220. Olga Shumsky Matlin, Ewing Lusk, and William McCune. 2002. SPINning Parallel Systems Software. In Model Checking of Software: 9th Intl. SPIN Workshop (LNCS), Dragan Bosnacki and Stefan Leue (Eds.), Vol. 2318. Springer, Berlin, Heidelberg, 213--220."},{"key":"e_1_3_2_1_14_1","volume-title":"MPI: A Message-Passing Interface Standard, Version 3.1","author":"Interface Forum Message-Passing","year":"2015","unstructured":"Message-Passing Interface Forum . 2015 . MPI: A Message-Passing Interface Standard, Version 3.1 . http:\/\/www.mpi-forum.org\/docs\/docs.html. (4 June 2015). Message-Passing Interface Forum. 2015. MPI: A Message-Passing Interface Standard, Version 3.1. http:\/\/www.mpi-forum.org\/docs\/docs.html. (4 June 2015)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.189.11"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999","author":"Shires Dale R.","year":"1999","unstructured":"Dale R. Shires , Lori L. Pollock , and Sara Sprenkle . 1999 . Program Flow Graph Construction For Static Analysis of MPI Programs . In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999 , June 28 -- July 1, 1999, Las Vegas, Nevada, USA, Hamid R. Arabnia (Ed.). CSREA Press, 1847--1853. Dale R. Shires, Lori L. Pollock, and Sara Sprenkle. 1999. Program Flow Graph Construction For Static Analysis of MPI Programs. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999, June 28 -- July 1, 1999, Las Vegas, Nevada, USA, Hamid R. Arabnia (Ed.). CSREA Press, 1847--1853."},{"key":"e_1_3_2_1_19_1","volume-title":"VMCAI 2007, Nice, France, January 14--16, 2007, Proceedings (LNCS), Byron Cook and Andreas Podelski (Eds.)","volume":"4349","author":"Siegel Stephen F.","year":"2007","unstructured":"Stephen F. Siegel . 2007 . Model Checking Nonblocking MPI Programs. In Verification, Model Checking, and Abstract Interpretation: 8th International Conference , VMCAI 2007, Nice, France, January 14--16, 2007, Proceedings (LNCS), Byron Cook and Andreas Podelski (Eds.) , Vol. 4349 . Springer, Berlin, Heidelberg, 44--58. Stephen F. Siegel. 2007. Model Checking Nonblocking MPI Programs. In Verification, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14--16, 2007, Proceedings (LNCS), Byron Cook and Andreas Podelski (Eds.), Vol. 4349. Springer, Berlin, Heidelberg, 44--58."},{"key":"e_1_3_2_1_20_1","volume-title":"Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, April 1--3, 2004, Proceedings (LNCS), Susanne Graf and Laurent Mounier (Eds.)","volume":"2989","author":"Stephen","unstructured":"Stephen F. Siegel and George S. Avrunin. 2004. Verification of MPI-based software for scientific computation . In Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, April 1--3, 2004, Proceedings (LNCS), Susanne Graf and Laurent Mounier (Eds.) , Vol. 2989 . Springer, Berlin, Heidelberg, 286--303. Stephen F. Siegel and George S. Avrunin. 2004. Verification of MPI-based software for scientific computation. In Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, April 1--3, 2004, Proceedings (LNCS), Susanne Graf and Laurent Mounier (Eds.), Vol. 2989. Springer, Berlin, Heidelberg, 286--303."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-011-0101-6"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-011-0100-7"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.2006.32"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_9"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"}],"event":{"name":"EuroMPI\/USA '17: 24th European MPI Users' Group Meeting","location":"Chicago Illinois","acronym":"EuroMPI\/USA '17","sponsor":["Mellanox Mellanox Technologies","Intel Intel","SIGHPC ACM Special Interest Group on High Performance Computing, Special Interest Group on High Performance Computing"]},"container-title":["Proceedings of the 24th European MPI Users' Group Meeting"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127024.3127032","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127024.3127032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:06Z","timestamp":1750212666000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127024.3127032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,25]]},"references-count":26,"alternative-id":["10.1145\/3127024.3127032","10.1145\/3127024"],"URL":"https:\/\/doi.org\/10.1145\/3127024.3127032","relation":{},"subject":[],"published":{"date-parts":[[2017,9,25]]},"assertion":[{"value":"2017-09-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}