{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:21:17Z","timestamp":1725560477091},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_20","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"286-303","source":"Crossref","is-referenced-by-count":25,"title":["Verification of MPI-Based Software for Scientific Computation"],"prefix":"10.1007","author":[{"given":"Stephen F.","family":"Siegel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George S.","family":"Avrunin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1109\/TIME.2001.930723","volume-title":"Proceedings of the Symposium on Temporal Representation and Reasoning (TIME 2001)","author":"B. Bollig","year":"2001","unstructured":"Bollig, B., Leucker, M.: Modelling, specifying, and verifying message passing systems. In: Bettini, C., Montanari, A. (eds.) Proceedings of the Symposium on Temporal Representation and Reasoning (TIME 2001), pp. 240\u2013248. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"CONCUR \u201998 Concurrency Theory","author":"E. Cohen","year":"1998","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 317\u2013331. Springer, Heidelberg (1998)"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01384316","volume":"6","author":"J.C. Corbett","year":"1995","unstructured":"Corbett, J.C., Avrunin, G.S.: Using integer programming to verify general safety and liveness properties. Formal Methods in System Design\u00a06, 97\u2013123 (1995)","journal-title":"Formal Methods in System Design"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/781131.781169","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Cytron, R., Gupta, R. (eds.) Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, San Diego, pp. 338\u2013349. ACM Press, New York (2003)"},{"key":"20_CR5","unstructured":"Georgelin, P., Pierre, L., Nguyen, T.: A formal specification of the MPI primitives and communication mechanisms. Technical Report 1999-337, LIM (1999)"},{"key":"20_CR6","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4789.001.0001","volume-title":"MPI\u2014The Complete Reference: the MPI Extensions","author":"W. Gropp","year":"1998","unstructured":"Gropp, W., Huss-Lederman, S., Lumsdaine, A., Lusk, E., Nitzberg, B., Saphir, W., Snir, M.: MPI\u2014The Complete Reference: the MPI Extensions, vol.\u00a02. MIT Press, Cambridge (1998)"},{"key":"20_CR7","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":"20_CR8","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Communications of the ACM\u00a018, 717\u2013721 (1975)","journal-title":"Communications of the ACM"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/BFb0054295","volume-title":"Mathematics of Program Construction","author":"R. Manohar","year":"1998","unstructured":"Manohar, R., Martin, A.J.: Slack elasticity in concurrent computing. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol.\u00a01422, pp. 272\u2013285. Springer, Heidelberg (1998)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-46017-9_16","volume-title":"Model Checking of Software: 9th International SPIN Workshop","author":"O.S. Matlin","year":"2002","unstructured":"Matlin, O.S., Lusk, E., McCune, W.: SPINning parallel systems software. In: Bonaki, D., Leue, S. (eds.) Model Checking of Software: 9th International SPIN Workshop, Grenoble. LNCS, vol.\u00a02318, pp. 213\u2013220. Springer, Heidelberg (2002)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","first-page":"279","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"A. Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0254, pp. 279\u2013324. Springer, Heidelberg (1987)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/3-540-45022-X_41","volume-title":"Automata, Languages and Programming, 27th International Colloquium, ICALP 2000","author":"B. Meenakshi","year":"2000","unstructured":"Meenakshi, B., Ramanujam, R.: Reasoning about message passing in finite state environments. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva. LNCS, vol.\u00a01853, pp. 487\u2013498. Springer, Heidelberg (2000)"},{"key":"20_CR13","unstructured":"Message-Passing Interface Standard 2.0 (1997), \n                    \n                      http:\/\/www.mpi-forum.org\/docs"},{"key":"20_CR14","unstructured":"Siegel, S.F.: The INCA query language. Technical Report UM-CS-2002-18, Department of Computer Science, University of Massachusetts (2002)"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/32.988494","volume":"28","author":"S.F. Siegel","year":"2002","unstructured":"Siegel, S.F., Avrunin, G.S.: Improving the precision of INCA by eliminating solutions with spurious cycles. IEEE Transactions on Software Engineering\u00a028, 115\u2013128 (2002)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"20_CR16","unstructured":"Siegel, S.F., Avrunin, G.S.: Analysis of MPI programs. Technical Report UM-CS- 2003-036, Department of Computer Science, University of Massachusetts (2003)"},{"key":"20_CR17","volume-title":"MPI\u2014The Complete Reference: The MPI Core","author":"M. Snir","year":"1998","unstructured":"Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI\u2014The Complete Reference: The MPI Core, 2nd edn., vol.\u00a01. MIT Press, Cambridge (1998)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T12:54:37Z","timestamp":1552827277000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}