{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:35Z","timestamp":1773655655780,"version":"3.50.1"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"12","license":[{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"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":["Commun. ACM"],"published-print":{"date-parts":[[2011,12]]},"abstract":"<jats:p>The goal is reliable parallel simulations, helping scientists understand nature, from how foams compress to how ribosomes construct proteins.<\/jats:p>","DOI":"10.1145\/2043174.2043194","type":"journal-article","created":{"date-parts":[[2011,11,21]],"date-time":"2011-11-21T19:54:36Z","timestamp":1321905276000},"page":"82-91","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Formal analysis of MPI-based parallel programs"],"prefix":"10.1145","volume":"54","author":[{"given":"Ganesh","family":"Gopalakrishnan","sequence":"first","affiliation":[{"name":"University of Utah, Salt Lake City, UT"}]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT"}]},{"given":"Stephen","family":"Siegel","sequence":"additional","affiliation":[{"name":"University of Delaware, Newark, DE"}]},{"given":"Rajeev","family":"Thakur","sequence":"additional","affiliation":[{"name":"Argonne National Laboratory, Argonne, IL"}]},{"given":"William","family":"Gropp","sequence":"additional","affiliation":[{"name":"University of Illinois in Urbana-Champaign"}]},{"given":"Ewing","family":"Lusk","sequence":"additional","affiliation":[{"name":"Argonne National Laboratory, Argonne, IL"}]},{"given":"Bronis R.","family":"De Supinski","sequence":"additional","affiliation":[{"name":"Lawrence Livermore National Laboratory, Livermore, CA"}]},{"given":"Martin","family":"Schulz","sequence":"additional","affiliation":[{"name":"Lawrence Livermore National Laboratory, Livermore, CA"}]},{"given":"Greg","family":"Bronevetsky","sequence":"additional","affiliation":[{"name":"Lawrence Livermore National Laboratory, Livermore, CA"}]}],"member":"320","published-online":{"date-parts":[[2011,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1654059.1654104"},{"key":"e_1_2_1_2_1","first-page":"10","article-title":"stack trace analysis for large-scale debugging. In","volume":"1","author":"Arnold D.C.","year":"2007","unstructured":"Arnold , D.C. , Ahn , D.H. , de supinski, B.R., Lee , G.L. , Miller , B.P. , and schulz, M . stack trace analysis for large-scale debugging. In Proceedings of the IEEE International Parallel & Distributed Processing Symposium (Long Beach, CA, Mar. 26--30). IEEE Computer Society , 2007 , 1 -- 10 . Arnold, D.C., Ahn, D.H., de supinski, B.R., Lee, G.L., Miller, B.P., and schulz, M. stack trace analysis for large-scale debugging. In Proceedings of the IEEE International Parallel & Distributed Processing Symposium (Long Beach, CA, Mar. 26--30). IEEE Computer Society, 2007, 1--10.","journal-title":"26--30). IEEE Computer Society"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/266469.266486"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770397"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/265932"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.32"},{"key":"e_1_2_1_7_1","volume-title":"Programming with POSIX Threads","author":"Butenhof D.R.","year":"2006","unstructured":"Butenhof , D.R. Programming with POSIX Threads . Addison-Wesley , Boston , 2006 . Butenhof, D.R. Programming with POSIX Threads. Addison-Wesley, Boston, 2006."},{"key":"e_1_2_1_8_1","first-page":"224","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the Eighth USENIX Symposium on Operating Systems Design and Implementation (San Diego, Dec. 7--10)","volume":"209","author":"Cadar C.","year":"2008","unstructured":"Cadar , C. , Dunbar , D. , and Engler , D . KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the Eighth USENIX Symposium on Operating Systems Design and Implementation (San Diego, Dec. 7--10) . USENIX Association , 2008 , 209 -- 224 . Cadar, C., Dunbar, D., and Engler, D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the Eighth USENIX Symposium on Operating Systems Design and Implementation (San Diego, Dec. 7--10). USENIX Association, 2008, 209--224.","journal-title":"USENIX Association"},{"key":"e_1_2_1_9_1","unstructured":"Eclipse Foundation Inc. Parallel Tools Platform. Ottawa Ontario Canada; http:\/\/www.eclipse.org\/ptp  Eclipse Foundation Inc. Parallel Tools Platform. Ottawa Ontario Canada; http:\/\/www.eclipse.org\/ptp"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_2_1_12_1","volume-title":"ISP Eclipse plug-in","author":"Graphical Explorer MPI","unstructured":"Graphical Explorer of MPI Programs . ISP Eclipse plug-in ; University of Utah , School of Computing; http:\/\/www.cs.utah.edu\/formal_verification\/GEM Graphical Explorer of MPI Programs. ISP Eclipse plug-in; University of Utah, School of Computing; http:\/\/www.cs.utah.edu\/formal_verification\/GEM"},{"key":"e_1_2_1_13_1","volume-title":"Using MPI-2: Portable Parallel Programming with the Message-Passing Interface","author":"Gropp W.","year":"1999","unstructured":"Gropp , W. , Lusk , E. , and Thakur , R . Using MPI-2: Portable Parallel Programming with the Message-Passing Interface . MIT Press , Cambridge, MA , 1999 . Gropp, W., Lusk, E., and Thakur, R. Using MPI-2: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge, MA, 1999."},{"key":"e_1_2_1_14_1","first-page":"66","article-title":"MUST: A scalable approach to runtime error detection in MPI programs. In Tools for High Performance Computing. Springer","volume":"53","author":"Hilbrich T.","year":"2009","unstructured":"Hilbrich , T. , Schulz , M. , de Supinski , B. , and M\u00fcller , M.S . MUST: A scalable approach to runtime error detection in MPI programs. In Tools for High Performance Computing. Springer , Berlin , 2009 , 53 -- 66 . Hilbrich, T., Schulz, M., de Supinski, B., and M\u00fcller, M.S. MUST: A scalable approach to runtime error detection in MPI programs. In Tools for High Performance Computing. Springer, Berlin, 2009, 53--66.","journal-title":"Berlin"},{"key":"e_1_2_1_15_1","unstructured":"International Exascale Software Project; http:\/\/www.exascale.org\/iesp\/Main_Page  International Exascale Software Project; http:\/\/www.exascale.org\/iesp\/Main_Page"},{"key":"e_1_2_1_16_1","volume-title":"ParMETIS: Parallel Graph Partitioning and Fill-Reducing Matrix Ordering","author":"Karypis Lab","unstructured":"Karypis Lab . ParMETIS: Parallel Graph Partitioning and Fill-Reducing Matrix Ordering . Minneapolis , MN ; http:\/\/glaros.dtc.umn.edu\/gkhome\/metis\/parmetis\/overview Karypis Lab. ParMETIS: Parallel Graph Partitioning and Fill-Reducing Matrix Ordering. Minneapolis, MN; http:\/\/glaros.dtc.umn.edu\/gkhome\/metis\/parmetis\/overview"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the Parallel Computing Conference (Dresden, Sept. 2--5","author":"Krammer B.","year":"2003","unstructured":"Krammer , B. , Bidmon , K. , M\u00fcjller , M.S. , and Resch , M.M . MARMOT: An MPI analysis and checking tool . In Proceedings of the Parallel Computing Conference (Dresden, Sept. 2--5 , 2003 ), 493--500. Krammer, B., Bidmon, K., M\u00fcjller, M.S., and Resch, M.M. MARMOT: An MPI analysis and checking tool. In Proceedings of the Parallel Computing Conference (Dresden, Sept. 2--5, 2003), 493--500."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_21_1","volume-title":"Version 2.2","author":"Message Passing Interface Forum","year":"2009","unstructured":"Message Passing Interface Forum . MPI: A Message-Passing Interface Standard , Version 2.2 , Sept. 4, 2009 ; http:\/\/www.mpi-forum.org\/docs\/ Message Passing Interface Forum. MPI: A Message-Passing Interface Standard, Version 2.2, Sept. 4, 2009; http:\/\/www.mpi-forum.org\/docs\/"},{"key":"e_1_2_1_22_1","unstructured":"MPICH2: High performance and widely portable MPI; http:\/\/www.mcs.anl.gov\/mpi\/mpich  MPICH2: High performance and widely portable MPI; http:\/\/www.mcs.anl.gov\/mpi\/mpich"},{"key":"e_1_2_1_23_1","unstructured":"Multicore Association. Multicore Communications API El Dorado Hills CA; http:\/\/www.multicore-association.org  Multicore Association. Multicore Communications API El Dorado Hills CA; http:\/\/www.multicore-association.org"},{"key":"e_1_2_1_24_1","unstructured":"NASA Advanced Supercomputing Division. Parallel Benchmarks; http:\/\/www.nas.nasa.gov\/Resources\/Software\/npb.html  NASA Advanced Supercomputing Division. Parallel Benchmarks ; http:\/\/www.nas.nasa.gov\/Resources\/Software\/npb.html"},{"key":"e_1_2_1_25_1","volume-title":"Open Source High Performance MPI","author":"Open MPI","unstructured":"Open MPI : Open Source High Performance MPI . Indiana University , Bloomington , IN; http:\/\/www.open-mpi.org\/ Open MPI: Open Source High Performance MPI. Indiana University, Bloomington, IN; http:\/\/www.open-mpi.org\/"},{"key":"e_1_2_1_26_1","volume-title":"Morgan Kaufmann","author":"Pacheco P.","year":"1996","unstructured":"Pacheco , P. Parallel Programming with MPI . Morgan Kaufmann , San Francisco , 1996 . Pacheco, P. Parallel Programming with MPI. Morgan Kaufmann, San Francisco, 1996."},{"key":"e_1_2_1_27_1","volume-title":"et al. The Toolkit for Accurate Scientific Software. Verified Software Laboratory","author":"Siegel S.F.","year":"2010","unstructured":"Siegel , S.F. et al. The Toolkit for Accurate Scientific Software. Verified Software Laboratory , University of Delaware , 2010 ; http:\/\/vsl.cis.udel.edu\/tass Siegel, S.F. et al. The Toolkit for Accurate Scientific Software. Verified Software Laboratory, University of Delaware, 2010; http:\/\/vsl.cis.udel.edu\/tass"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348256"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.2006.32"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_46"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/370049.370462"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.64"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504214"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2043174.2043194","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2043174.2043194","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:54:38Z","timestamp":1750240478000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2043174.2043194"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":34,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["10.1145\/2043174.2043194"],"URL":"https:\/\/doi.org\/10.1145\/2043174.2043194","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"2011-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}