{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T02:10:40Z","timestamp":1739412640126,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_46","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"724-740","source":"Crossref","is-referenced-by-count":10,"title":["Reduced Execution Semantics of MPI: From Theory to Practice"],"prefix":"10.1007","author":[{"given":"Sarvani","family":"Vakkalanka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anh","family":"Vo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"46_CR1","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using Verisoft. In: POPL, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"46_CR2","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/1040305.1040315","volume-title":"POPL","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110\u2013121. ACM, New York (2005)"},{"key":"46_CR3","unstructured":"The Java Pathfinder, http:\/\/javapathfinder.sourceforge.net"},{"key":"46_CR4","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 446\u2013455 (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"46_CR5","unstructured":"CHESS: Find and Reproduce Heisenbugs in Concurrent Programs, http:\/\/research.microsoft.com\/en-us\/projects\/chess\/"},{"key":"46_CR6","doi-asserted-by":"crossref","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Wang, C.: Automatic Discovery of Transition Symmetry in Multithreaded Programs using Dynamic Analysis. In: SPIN 2009, Grenoble (June 2009)","DOI":"10.1007\/978-3-642-02652-2_22"},{"key":"46_CR7","unstructured":"MPI Standard 2.1., http:\/\/www.mpi-forum.org\/docs\/"},{"key":"46_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-70545-1_9","volume-title":"Computer Aided Verification","author":"S. Vakkalanka","year":"2008","unstructured":"Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M.: Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 66\u201379. Springer, Heidelberg (2008)"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical mpi programs. In: PPoPP 2009 (2009)","DOI":"10.1145\/1594835.1504214"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: Scheduling considerations for building dynamic verification tools for MPI. In: PADTAD-VI 2008 (2008)","DOI":"10.1145\/1390841.1390844"},{"key":"46_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/978-3-642-03770-2_43","volume-title":"EuroPCM\/MPI 2009","author":"S. Vakkalanka","year":"2009","unstructured":"Vakkalanka, S., et al.: Static-analysis Assisted Dynamic Verification of MPI Waitany Programs (Poster Abstract). In: Ropo, M., Westerholm, J., Dongarra, J. (eds.) EuroPCM\/MPI 2009. LNCS, vol.\u00a05759, p. 329. Springer, Heidelberg (2009)"},{"key":"46_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-642-03770-2_33","volume-title":"EuroPCM\/MPI 2009","author":"A. Vo","year":"2009","unstructured":"Vo, A., et al.: Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-Determinism. In: Ropo, M., Westerholm, J., Dongarra, J. (eds.) EuroPCM\/MPI 2009. LNCS, vol.\u00a05759, pp. 271\u2013281. Springer, Heidelberg (2009)"},{"key":"46_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-79707-4_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"R. Palmer","year":"2008","unstructured":"Palmer, R., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: An Approach to Formalization and Analysis of Message Passing Libraries. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 164\u2013181. Springer, Heidelberg (2008)"},{"key":"46_CR14","unstructured":"Li, G., et al.: Formal Specification of the MPI 2.0 Standard in TLA+. Under Submission, http:\/\/www.cs.utah.edu\/formal_verification\/mpitla\/"},{"key":"46_CR15","volume-title":"Specifying Systems: The TLA Language and Tools","author":"L. Lamport","year":"2004","unstructured":"Lamport, L.: Specifying Systems: The TLA Language and Tools. Addison-Wesley, Reading (2004)"},{"key":"46_CR16","doi-asserted-by":"crossref","unstructured":"Karypis, G., Kumar, V.: Parallel multilevel k-way partitioning scheme for irregular graphs. In: SuperComputing, SC (1996)","DOI":"10.1145\/369028.369103"},{"key":"46_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-87475-1_31","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"S.F. Siegel","year":"2008","unstructured":"Siegel, S.F., Siegel, A.R.: MADRE: The Memory-Aware Data Redistribution Engine. In: Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.) EuroPVM\/MPI 2008. LNCS, vol.\u00a05205, pp. 218\u2013226. Springer, Heidelberg (2008)"},{"key":"46_CR18","unstructured":"Workshop on Exploiting Concurrency Efficiently and Correctly, Grenoble, Discussion of Challenge Problems (June 2009), http:\/\/www.cs.utah.edu\/ec2"},{"key":"46_CR19","volume-title":"Parallel Programming with MPI","author":"P. Pacheco","year":"1996","unstructured":"Pacheco, P.: Parallel Programming with MPI. Morgan Kaufmann, San Francisco (1996)"},{"key":"46_CR20","unstructured":"DeLisi, M.: Umpire Test Suite Results using ISP, http:\/\/www.cs.utah.edu\/formal_verification\/ISP_Tests\/"},{"issue":"7","key":"46_CR21","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM\u00a021(7), 558\u2013564 (1978)","journal-title":"Communications of the ACM"},{"key":"46_CR22","doi-asserted-by":"crossref","unstructured":"Siegel, S.F.: Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. In: VMCAI 2006, pp.\u00a0413\u2013429 (2006)","DOI":"10.1007\/978-3-540-30579-8_27"},{"key":"46_CR23","unstructured":"Georgelin, P., Pierre, L., Nguyen, T.: A Formal Specification of the MPI Primitives and Communication Mechanisms. Rapport de Recherche LIM 1999-337, Marseille (October 1999)"},{"key":"46_CR24","unstructured":"http:\/\/www.cs.utah.edu\/formal_verification\/ISP-release\/"},{"key":"46_CR25","unstructured":"mpiBLAST: Open-Source Parallel BLAST, http:\/\/www.mpiblast.org\/"},{"key":"46_CR26","unstructured":"The IRS Benchmark Code, https:\/\/asc.llnl.gov\/computing_resources\/purple\/archive\/benchmarks\/irs\/"},{"key":"46_CR27","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"46_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/BFb0056008","volume-title":"Mathematics of Program Construction","author":"R. Martin","year":"1998","unstructured":"Martin, R., Manohar, A.: Slack Elasticity in Concurrent Computing. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol.\u00a01422, p. 272. Springer, Heidelberg (1998)"},{"key":"46_CR29","doi-asserted-by":"crossref","unstructured":"Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC - A runtime verification tool for MCAPI user applications. In: FMCAD 2009, Austin (accepted, 2009)","DOI":"10.1109\/FMCAD.2009.5351145"},{"key":"46_CR30","unstructured":"The Multicore Communications API (MCAPI), http:\/\/www.multicore-association.org"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T01:53:28Z","timestamp":1739411608000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}