{"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":1773655655190,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705437","type":"print"},{"value":"9783540705451","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_9","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"66-79","source":"Crossref","is-referenced-by-count":47,"title":["Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings"],"prefix":"10.1007","author":[{"given":"Sarvani","family":"Vakkalanka","sequence":"first","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"MPI-The Complete Reference: The MPI Core","author":"M. Snir","year":"1998","unstructured":"Snir, M., Otto, S.: MPI-The Complete Reference: The MPI Core. MIT Press, Cambridge (1998)"},{"key":"9_CR2","unstructured":"Invited Talk by Al Geist at EuroPVM\/MPI 2007, Sustained Petascale: The Next MPI Challenge"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Krammer, B., Bidmon, K., M\u00fcller, M.S., Resch, M.M.: Marmot: An MPI analysis and checking tool. In: Parallel Computing 2003 (September 2003)","DOI":"10.1016\/S0927-5452(04)80063-7"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Vetter, J.S., de Supinski, B.R.: Dynamic software testing of MPI applications with Umpire. In: Supercomputing, pp. 70\u201379 (2000)","DOI":"10.1109\/SC.2000.10055"},{"key":"9_CR5","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":"9_CR6","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: Palsberg, J., Abadi, M. (eds.) POPL, pp. 110\u2013121. ACM, New York (2005)"},{"issue":"7","key":"9_CR7","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\u2013565 (1978)","journal-title":"Communications of the ACM"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Palmer, R., Gopalakrishnan, G., Kirby, R.M.: Semantics driven dynamic partial-order reduction of MPI-based parallel programs. In: Parallel and Distributed Systems - Testing and Debugging (PADTAD-V) (July 2007)","DOI":"10.1145\/1273647.1273657"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Pervez, S., Palmer, R., Gopalakrishnan, G., Kirby, R.M., Thakur, R., Gropp, W.: Practical model checking method for verifying correctness of MPI programs. In: EuroPVM\/MPI, pp. 344\u2013353 (2007)","DOI":"10.1007\/978-3-540-75416-9_46"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Vakkalanka, S., Sharma, S.V., Gopalakrishnan, G., Kirby, R.M.: ISP: A tool for model checking MPI programs. In: Principles and Practices of Parallel Programming (PPoPP), pp. 285\u2013286 (2008)","DOI":"10.1145\/1345206.1345258"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Li, G., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: Formal specification of the MPI-2.0 standard in TLA+. In: Principles and Practices of Parallel Programming (PPoPP), pp. 283\u2013284 (2008)","DOI":"10.1145\/1345206.1345257"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-3-540-30579-8_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.F. Siegel","year":"2005","unstructured":"Siegel, S.F.: Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 413\u2013429. Springer, Heidelberg (2005)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Avrunin, G.S.: Modeling Wildcard-free MPI Programs for Verification. In: Proceedings of the ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming (to appear, 2005)","DOI":"10.1145\/1065944.1065957"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: Proceedings of the 11th International SPIN Workshop on Model Checking Software, Barcelona, April 2004, pp. 286\u2013303 (2004)","DOI":"10.1007\/978-3-540-24732-6_20"},{"key":"9_CR15","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"9_CR16","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: UUCS-07-008:Runtime Model Checking of Multithreaded C\/C++ Programs. Technical report, University of Utah, School of Computing (2007), http:\/\/www.cs.utah.edu\/research\/techreports\/2007\/ps\/UUCS-07-008.ps"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-73370-6_6","volume-title":"Model Checking Software","author":"Y. Yang","year":"2007","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Distributed dynamic partial order reduction based verification of threaded software. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 58\u201375. Springer, Heidelberg (2007)"},{"key":"9_CR18","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, pp. 446\u2013455 (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"9_CR19","unstructured":"http:\/\/research.microsoft.com\/projects\/CHESS\/"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Vuduc, R., Schulz, M., Quinlan, D., de Supinski, B., Saebjornsen, A.: Improved distributed memory applications testing by message perturbation. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD - IV) (2006)","DOI":"10.1145\/1147403.1147409"},{"key":"9_CR21","unstructured":"Sharma, S.V., Gopalakrishnan, G., Kirby, R.M.: A survey of MPI related debuggers and tools. Technical Report UUCS-07-015, University of Utah, School of Computing (2007), http:\/\/www.cs.utah.edu\/research\/techreports.shtml"},{"issue":"3-5","key":"9_CR22","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1002\/cpe.654","volume":"15","author":"O. Edelstein","year":"2003","unstructured":"Edelstein, O., Farchi, E., Goldin, E., Nir, Y., Ratsaby, G., Ur, S.: Framework for testing multi-threaded Java programs. Concurrency and Computation: Practice and Experience\u00a015(3-5), 485\u2013499 (2003)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"9_CR23","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"9_CR24","unstructured":"Palmer, R., Delisi, M., Gopalakrishnan, G., Kirby, R.M.: An approach to formalization and analysis of message passing libraries. In: Formal Methods for Industry Critical Systems (FMICS), Berlin (2007)"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"DeSouza, J., Kuhn, B., de Supinski, B.R., Samofalov, V., Zheltov, S., Bratanov, S.: Automated, scalable debugging of MPI programs with intel message checker. In: SE-HPCS 2005, pp. 78\u201382 (2005)","DOI":"10.1145\/1145319.1145342"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T14:50:13Z","timestamp":1684507813000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}