{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:01:16Z","timestamp":1767927676453,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540754152","type":"print"},{"value":"9783540754169","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75416-9_46","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T05:37:56Z","timestamp":1189748276000},"page":"344-353","source":"Crossref","is-referenced-by-count":10,"title":["Practical Model-Checking Method for Verifying Correctness of MPI Programs"],"prefix":"10.1007","author":[{"given":"Salman","family":"Pervez","sequence":"first","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Palmer","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Thakur","sequence":"additional","affiliation":[]},{"given":"William","family":"Gropp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"46_CR1","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (1999)"},{"key":"46_CR2","doi-asserted-by":"crossref","unstructured":"Souza, J.D., Kuhn, B., de Supinski, B.R., Samofalov, V., Zheltov, S., Bratanov, 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"},{"key":"46_CR3","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110\u2013121 (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"46_CR4","unstructured":"Gao, Q., Yu, W., Huang, W., Panda, D.K.: Application-transparent checkpoint\/restart for MPI programs over InfiniBand. In: ICPP (August 2006)"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: POPL 1997: Principles of Programming Languages, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"46_CR6","volume-title":"The Spin Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Reading (2003)"},{"key":"46_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/11846802_21","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"B. Krammer","year":"2006","unstructured":"Krammer, B., Resch, M.M.: Correctness checking of MPI one-sided communication using MARMOT. In: Mohr, B., Tr\u00e4ff, J.L., Worringen, J., Dongarra, J. (eds.) Recent Advances in Parallel Virtual Machine and Message Passing Interface. LNCS, vol.\u00a04192, pp. 105\u2013114. Springer, Heidelberg (2006)"},{"key":"46_CR8","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1002\/cpe.705","volume":"15","author":"G. Luecke","year":"2003","unstructured":"Luecke, G., Chen, H., Coyle, J., Hoekstra, J., Kraeva, M., Zou, Y.: MPI-CHECK: A tool for checking Fortran 90 MPI programs. Concurrency and Computation: Practice and Experience\u00a015, 93\u2013100 (2003)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"46_CR9","unstructured":"Palmer, R., Barrus, S., Yang, Y., Gopalakrishnan, G., Kirby, R.M.: Gauss: A framework for verifying scientific computing software. In: Workshop on Software Model Checking. ENTCS 953 (2005)"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Palmer, R., Gopalakrishnan, G., Kirby, R.M.: Semantics driven dynamic partial-order reduction of MPI-based parallel programs. In: PADTAD (2007)","DOI":"10.1145\/1273647.1273657"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"Pervez, S., Gopalakrishnan, G., Kirby, R.M., Thakur, R., Gropp, W.: Formal verification of programs that use MPI one-sided communication. In: EuroPVM\/MPI, pp. 30\u201339 (2006)","DOI":"10.1007\/11846802_13"},{"key":"46_CR12","unstructured":"Preliminary release of the ISP software at http:\/\/www.cs.utah.edu\/formal_verification\/isp.tar.gz"},{"key":"46_CR13","doi-asserted-by":"crossref","unstructured":"Siegel, S.F.: Model checking nonblocking MPI programs. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (January 2007)","DOI":"10.1007\/978-3-540-69738-1_3"},{"key":"46_CR14","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: SPIN Workshop, pp. 286\u2013303 (April 2004)","DOI":"10.1007\/978-3-540-24732-6_20"},{"key":"46_CR15","doi-asserted-by":"crossref","unstructured":"Thakur, R., Ross, R., Latham, R.: Implementing byte-range locks using MPI one-sided communication. In: EuroPVM\/MPI, pp. 120\u2013129 (September 2005)","DOI":"10.1007\/11557265_19"},{"key":"46_CR16","doi-asserted-by":"crossref","unstructured":"Vetter, J.S., de Supinski, B.R.: Dynamic software testing of MPI applications with Umpire. In: Proc. of SC2000, pp. 70\u201379 (2000)","DOI":"10.1109\/SC.2000.10055"},{"key":"46_CR17","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: ASE (September 2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"46_CR18","doi-asserted-by":"crossref","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Distributed dynamic partial order reduction based verification of threaded software. In: Workshop on Model Checking Software (SPIN 2007) (July 2007)","DOI":"10.1007\/978-3-540-73370-6_6"}],"container-title":["Lecture Notes in Computer Science","Recent Advances in Parallel Virtual Machine and Message Passing Interface"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75416-9_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:01:25Z","timestamp":1619521285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75416-9_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540754152","9783540754169"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75416-9_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}