{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:02Z","timestamp":1725511862094},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797067"},{"type":"electronic","value":"9783540797074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79707-4_13","type":"book-chapter","created":{"date-parts":[[2008,5,7]],"date-time":"2008-05-07T06:37:44Z","timestamp":1210142264000},"page":"164-181","source":"Crossref","is-referenced-by-count":5,"title":["An Approach to Formalization and Analysis of Message Passing Libraries"],"prefix":"10.1007","author":[{"given":"Robert","family":"Palmer","sequence":"first","affiliation":[]},{"given":"Michael","family":"DeLisi","sequence":"additional","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"The Message Passing Interface Forum: MPI: A Message-Passing Interface Standard (1995), http:\/\/www.mpi-forum.org\/docs\/mpi-11-html\/mpi-report.html"},{"issue":"6","key":"13_CR2","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1016\/0167-8191(96)00024-5","volume":"22","author":"W. Gropp","year":"1996","unstructured":"Gropp, W., Lusk, E.L., Doss, N.E., Skjellum, A.: A high-performance, portable implementation of the mpi message passing interface standard. Parallel Computing\u00a022(6), 789\u2013828 (1996)","journal-title":"Parallel Computing"},{"key":"13_CR3","unstructured":"Microsoft: Microsoft windows compute cluster 2003 (2006), www.microsoft.com\/windowsserver2003\/ccs\/faq.mspx"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-540-39924-7_52","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"J.M. Squyres","year":"2003","unstructured":"Squyres, J.M., Lumsdaine, A.: A Component Architecture for LAM\/MPI. In: Dongarra, J., Laforenza, D., Orlando, S. (eds.) EuroPVM\/MPI 2003. LNCS, vol.\u00a02840, pp. 379\u2013387. Springer, Heidelberg (2003)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Gabriel, E., Fagg, G.E., Bosilca, G., Angskun, T., Dongarra, J.J., Squyres, J.M., Sahay, V., Kambadur, P., Barrett, B., Lumsdaine, A., Castain, R.H., Daniel, D.J., Graham, R.L., Woodall, T.S.: Open MPI: Goals, concept, and design of a next generation MPI implementation. In: Proceedings, 11th European PVM\/MPI Users\u2019 Group Meeting, Budapest, Hungary, pp. 97\u2013104 (2004)","DOI":"10.1007\/978-3-540-30218-6_19"},{"key":"13_CR6","first-page":"58","volume-title":"SC 2005: Proceedings of the 2005 ACM\/IEEE conference on Supercomputing","author":"A. Danalis","year":"2005","unstructured":"Danalis, A., Kim, K.Y., Pollock, L., Swany, M.: Transformations to parallel codes for communication-computation overlap. In: SC 2005: Proceedings of the 2005 ACM\/IEEE conference on Supercomputing, Washington, DC, USA, p. 58. IEEE Computer Society, Los Alamitos (2005)"},{"key":"13_CR7","unstructured":"Lamport, L.: Specifying concurrent systems with TLA (1999)"},{"key":"13_CR8","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 54\u201366. Springer, Heidelberg (1999)"},{"key":"13_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 (2007), http:\/\/www.cs.utah.edu\/formal_verification\/verification_environment","DOI":"10.1145\/1273647.1273657"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1040305.1040315","volume-title":"POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 110\u2013121. ACM Press, New York (2005)"},{"key":"13_CR12","unstructured":"IEEE: IEEE Standard for Radix-independent Floating-point Arithmetic, ANSI\/IEEE Std 854\u20131987 (1987)"},{"key":"#cr-split#-13_CR13.1","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal verification of square root algorithms. Formal Methods in System Design??22(2), 143???154 (2003);","DOI":"10.1023\/A:1022973506233"},{"key":"#cr-split#-13_CR13.2","unstructured":"Guest Editors: Gopalakrishnan, G., Hunt, W., Jr."},{"key":"13_CR14","unstructured":"Lamport, L.: The Win32 Threads API Specification (1996), http:\/\/research.microsoft.com\/users\/lamport\/tla\/threads\/threads.html"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L., Merz, S.: A tla solution to the rpc-memory specification problem. In: Formal Systems Specification, pp. 21\u201366 (1994)","DOI":"10.1007\/BFb0024426"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering Methodologies\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering Methodologies"},{"key":"13_CR17","first-page":"730","volume-title":"ICSE 2000: Proceedings of the 22nd international conference on Software engineering","author":"D. Jackson","year":"2000","unstructured":"Jackson, D., Schechter, I., Shlyahter, H.: Alcoa: The alloy constraint analyzer. In: ICSE 2000: Proceedings of the 22nd international conference on Software engineering, pp. 730\u2013733. ACM Press, New York (2000)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A new technology for software modeling. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280. Springer, Heidelberg (2002)"},{"key":"13_CR19","unstructured":"Georgelin, P., Pierre, L., Nguyen, T.: A formal specification of the MPI primitives and communication mechanisms. Technical report, LIM (1999)"},{"volume-title":"Formal Description Technique Lotos: Results of the Esprit Sedos Project","year":"1989","key":"13_CR20","unstructured":"Eijk, P.V., Diaz, M. (eds.): Formal Description Technique Lotos: Results of the Esprit Sedos Project. Elsevier Science Inc., New York, NY, USA (1989)"},{"key":"13_CR21","unstructured":"Siegel, S.F., Avrunin, G.: Analysis of mpi programs. Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts Amherst (2003)"},{"issue":"5","key":"13_CR22","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Avrunin, G.S.: Modeling wildcard-free MPI programs for verification. In: SIGPLAN Symposium, A.C.M. (ed.) ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming, Chicago, pp. 95\u2013106 (2005)","DOI":"10.1145\/1065944.1065957"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-69738-1_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.F. Siegel","year":"2007","unstructured":"Siegel, S.F.: Model Checking Nonblocking MPI Programs. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 44\u201358. Springer, Heidelberg (2007)"},{"key":"13_CR25","unstructured":"Barrus, S., Gopalakrishnan, G., Kirby, R.M., Palmer, R.: Verification of MPI programs using SPIN. Technical Report UUCS-04-008, The University of Utah (2004)"},{"key":"13_CR26","unstructured":"Palmer, R., Barrus, S., Yang, Y., Gopalakrishnan, G., Kirby, R.M.: Gauss: A framework for verifying scientific computing software. In: SoftMC: Workshop on Software Model Checking. ENTCS, vol.\u00a0953 (2005)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","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., Gopalakrishnan, G., Kirby, R.M., Thakur, R., Gropp, W.: Formal verification of programs that use MPI one-sided communication. In: Mohr, B., Tr\u00e4ff, J.L., Worringen, J., Dongarra, J. (eds.) PVM\/MPI 2006. LNCS, vol.\u00a04192, pp. 30\u201339. Springer, Berlin, Heidelberg (2006)"},{"key":"13_CR28","unstructured":"Palmer, R., Gopalakrishnan, G., Kirby, R.M.: The communication semantics of the message passing interface. Technical Report UUCS-06-012, The University of Utah (2006)"},{"key":"13_CR29","unstructured":"Gropp, W.D.: Personal communication (2006)"},{"key":"13_CR30","unstructured":"Microsoft: Phoenix academic program (2007), http:\/\/research.microsoft.com\/phoenix"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-45848-4_57","volume-title":"Graph Drawing","author":"J. Ellson","year":"2002","unstructured":"Ellson, J., Gansner, E., Koutsofios, L., North, S.C., Woodhull, G.: Graphviz \u2013 open source graph drawing tools. In: Mutzel, P., J\u00fcnger, M., Leipert, S. (eds.) GD 2001. LNCS, vol.\u00a02265, p. 483. Springer, Heidelberg (2002)"},{"key":"13_CR32","unstructured":"Lamport, L.: A +CAL user\u2019s manual (2006), http:\/\/research.microsoft.com\/users\/lamport\/tla\/p-manual.pdf"},{"key":"13_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA (1999)"},{"key":"13_CR34","volume-title":"Parallel programming with MPI","author":"P.S. Pacheco","year":"1996","unstructured":"Pacheco, P.S.: Parallel programming with MPI. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1996)"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/11846802_11","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"W. Gropp","year":"2006","unstructured":"Gropp, W., Thakur, R.: Issues in developing a thread-safe MPI implementation. In: Mohr, B., Tr\u00e4ff, J.L., Worringen, J., Dongarra, J. (eds.) PVM\/MPI 2006. LNCS, vol.\u00a04192, pp. 12\u201321. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79707-4_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:28:37Z","timestamp":1619522917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79707-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797067","9783540797074"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79707-4_13","relation":{},"subject":[]}}