{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:39Z","timestamp":1773655659972,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540697350","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_3","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"44-58","source":"Crossref","is-referenced-by-count":35,"title":["Model Checking Nonblocking MPI Programs"],"prefix":"10.1007","author":[{"given":"Stephen F.","family":"Siegel","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","volume-title":"The Spin Model Checker","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","first-page":"11","volume-title":"Model Checking Software","author":"O.S. Matlin","year":"2002","unstructured":"Matlin, O.S., Lusk, E., McCune, W.: SPINning parallel systems software. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) Model Checking Software. LNCS, vol.\u00a02318, pp. 11\u201313. Springer, Heidelberg (2002)"},{"key":"3_CR3","unstructured":"Message Passing Interface Forum: MPI: A Message-Passing Interface standard, version 1.1, \n                    \n                      http:\/\/www.mpi-forum.org\/docs\/\n                    \n                    \n                   (1995)"},{"key":"3_CR4","unstructured":"Message Passing Interface Forum: MPI-2: Extensions to the Message-Passing Interface. \n                    \n                      http:\/\/www.mpi-forum.org\/docs\/\n                    \n                    \n                   (1997)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11846802_13","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"S. Pervez","year":"2006","unstructured":"Pervez, S., et al.: Formal verification of programs that use MPI one-sided communication. In: Mohr, B., et al. (eds.) Recent Advances in Parallel Virtual Machine and Message Passing Interface. LNCS, vol.\u00a04192, Springer, Heidelberg (2006)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Post, D.E., Votta, L.G.: Computational science demands a new paradigm. Physics Today, 35\u201341 (January 2005)","DOI":"10.1063\/1.1881898"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","first-page":"17","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. 17\u201319. Springer, Heidelberg (2005)"},{"key":"3_CR8","unstructured":"Siegel, S.F., Avrunin, G.S.: Modeling MPI programs for verification. Technical Report UM-CS-2004-75, Department of Computer Science, University of Massachusetts (2004)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Model Checking Software","author":"S.F. Siegel","year":"2004","unstructured":"Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol.\u00a02989, pp. 1\u20133. Springer, Heidelberg (2004)"},{"key":"3_CR10","first-page":"15","volume-title":"Proceedings of the 2005 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","author":"S.F. Siegel","year":"2005","unstructured":"Siegel, S.F., Avrunin, G.S.: Modeling wildcard-free MPI programs for verification. In: Proceedings of the 2005 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP\u201905, Chicago, Illinois, USA, June 15\u201317, 2005, pp. 15\u201317. ACM Press, New York (2005)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Pollock, L., Pezz\u00e9, M.(eds.). ISSTA 2006: Proceedings of the ACM SIGSOFT 2006 International Symposium on Software Testing and Analysis, Portland, ME, pp. 157\u2013168 (2006)","DOI":"10.1145\/1146238.1146256"},{"key":"3_CR12","unstructured":"Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI\u2014The Complete Reference, Volume 1: The MPI Core. MIT Press, second edition (1998)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:45:09Z","timestamp":1620017109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_3","relation":{},"subject":[]}}