{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:24:49Z","timestamp":1725470689308},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540391104"},{"type":"electronic","value":"9783540391128"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11846802_13","type":"book-chapter","created":{"date-parts":[[2006,9,16]],"date-time":"2006-09-16T06:27:41Z","timestamp":1158388061000},"page":"30-39","source":"Crossref","is-referenced-by-count":19,"title":["Formal Verification of Programs That Use MPI One-Sided Communication"],"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":"Rajeev","family":"Thakur","sequence":"additional","affiliation":[]},{"given":"William","family":"Gropp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"13_CR2","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":"13_CR3","volume-title":"Using MPI-2: Advanced Features of the Message-Passing Interface","author":"W. Gropp","year":"1999","unstructured":"Gropp, W., Lusk, E., Thakur, R.: Using MPI-2: Advanced Features of the Message-Passing Interface. MIT Press, Cambridge (1999)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11557265_53","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"W. Gropp","year":"2005","unstructured":"Gropp, W., Thakur, R.: An evaluation of implementation options for MPI one-sided communication. In: Di Martino, B., Kranzlm\u00fcller, D., Dongarra, J. (eds.) EuroPVM\/MPI 2005. LNCS, vol.\u00a03666, pp. 415\u2013424. Springer, Heidelberg (2005)"},{"key":"13_CR5","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"unstructured":"Kranzlm\u00fcller, D.: Event Graph Analysis for Debugging Massively Parallel Programs. PhD thesis, John Kepler University Linz, Austria (September 2000), \n                    \n                      http:\/\/www.gup.uni-linz.ac.at\/dk\/thesis","key":"13_CR6"},{"unstructured":"L. Lamport.: \n                    \n                      http:\/\/research.microsoft.com\/users\/lamport\/tla\/pluscal.html","key":"13_CR7"},{"issue":"10","key":"13_CR8","doi-asserted-by":"publisher","first-page":"1037","DOI":"10.1002\/cpe.796","volume":"16","author":"G.R. Luecke","year":"2004","unstructured":"Luecke, G.R., Spanoyannis, S., Kraeva, M.: The performance and scalability of SHMEM and MPI-2 one-sided routines on a SGI Origin 2000 and a Cray T3E-600. Concurrency and Computation: Practice and Experience\u00a016(10), 1037\u20131060 (2004)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-46017-9_16","volume-title":"Model Checking Software","author":"O. Shumsky Matlin","year":"2002","unstructured":"Shumsky Matlin, O., Lusk, E., McCune, W.: SPINning parallel systems software. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 213\u2013220. Springer, Heidelberg (2002)"},{"unstructured":"Message Passing Interface Forum. MPI-2: Extensions to the Message-Passing Interface (July 1997), \n                    \n                      http:\/\/www.mpi-forum.org\/docs\/docs.html","key":"13_CR10"},{"unstructured":"S. Pervez.: \n                    \n                       http:\/\/www.cs.utah.edu\/spervez\/model.tar.gz","key":"13_CR11"},{"unstructured":"Pervez, S.: Byte-range locks using MPI one-sided communication. Technical report, University of Utah, School of Computing (2006), \n                    \n                      http:\/\/www.cs.utah.edu\/formal_verification\/OnesidedTR1\/","key":"13_CR12"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-540-24732-6_20","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.) SPIN 2004. LNCS, vol.\u00a02989, pp. 286\u2013303. Springer, Heidelberg (2004)"},{"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: Proceedings of the ACM SIGSOFT 2006 International Symposium on Software Testing and Analysis (July 2006)","key":"13_CR14","DOI":"10.1145\/1146238.1146256"},{"key":"13_CR15","volume-title":"Modern Operating Systems","author":"A.S. Tanenbaum","year":"2001","unstructured":"Tanenbaum, A.S.: Modern Operating Systems. Prentice-Hall, Inc., Englewood Cliffs (2001)"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1177\/1094342005054258","volume":"19","author":"R. Thakur","year":"2005","unstructured":"Thakur, R., Gropp, W., Toonen, B.: Optimizing the synchronization operations in MPI one-sided communication. International Journal of High-Performance Computing Applications\u00a019(2), 119\u2013128 (2005)","journal-title":"International Journal of High-Performance Computing Applications"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/11557265_19","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"R. Thakur","year":"2005","unstructured":"Thakur, R., Ross, R., Latham, R.: Implementing byte-range locks using MPI one-sided communication. In: Di Martino, B., Kranzlm\u00fcller, D., Dongarra, J. (eds.) EuroPVM\/MPI 2005. LNCS, vol.\u00a03666, pp. 119\u2013128. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Recent Advances in Parallel Virtual Machine and Message Passing Interface"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11846802_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:18:18Z","timestamp":1619507898000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11846802_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540391104","9783540391128"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11846802_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}