{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:06:51Z","timestamp":1742911611818,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182747"},{"type":"electronic","value":"9783642182754"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_2","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T00:06:38Z","timestamp":1295222798000},"page":"2-18","source":"Crossref","is-referenced-by-count":11,"title":["Formal Analysis of Message Passing"],"prefix":"10.1007","author":[{"given":"Stephen F.","family":"Siegel","sequence":"first","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Armstrong, J.: Programming in Erlang: Software for a Concurrent World. Pragmatic Bookshelf (July 2007)"},{"issue":"10","key":"2_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/1562764.1562783","volume":"52","author":"K. Asanovic","year":"2009","unstructured":"Asanovic, K., Bodik, R., Demmel, J., Keaveny, T., Keutzer, K., Kubiatowicz, J., Morgan, N., Patterson, D., Sen, K., Wawrzynek, J., Wessel, D., Yelick, K.: A view of the parallel computing landscape. Comm. ACM\u00a052(10), 56\u201367 (2009)","journal-title":"Comm. ACM"},{"key":"2_CR3","unstructured":"Atzeni, S.: ISP takes Steve\u2019s midterm exam, \n                  \n                    http:\/\/www.cs.utah.edu\/~simone\/Steve_Midterm_Exam\/"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"2_CR5","first-page":"1","volume-title":"Proceedings of The Seventh International Symposium on Code Generation and Optimization","author":"G. Bronevetsky","year":"2009","unstructured":"Bronevetsky, G.: Communication-sensitive static dataflow for parallel message passing applications. In: Proceedings of The Seventh International Symposium on Code Generation and Optimization, pp. 1\u201312. IEEE Computer Society, Los Alamitos (2009)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","year":"2007","unstructured":"Cappello, F., H\u00e9rault, T., Dongarra, J. (eds.): PVM\/MPI 2007. LNCS, vol.\u00a04757. Springer, Heidelberg (2007)"},{"key":"2_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-10003-2_65","volume-title":"Automata, Languages and Programming","author":"P. Cousot","year":"1980","unstructured":"Cousot, P., Cousot, R.: Semantic analysis of communicating sequential processes. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 119\u2013133. Springer, Heidelberg (1980)"},{"key":"2_CR9","unstructured":"DeLisi, M.: Test results comparing ISP, Marmot, and mpirun, \n                  \n                    http:\/\/www.cs.utah.edu\/fv\/ISP_Tests"},{"key":"2_CR10","first-page":"43","volume-title":"Programming Languages: NATO Advanced Study Inst.","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Inst., pp. 43\u2013112. Academic Press, London (1968)"},{"key":"2_CR11","first-page":"174","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997","author":"P. Godefroid","year":"1997","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 174\u2013186. ACM, New York (1997)"},{"key":"2_CR12","unstructured":"Gopalakrishnan, G.L., Kirby, R.M.: Top ten ways to make formal methods for HPC practical. In: 2010 FSE\/SDP Workshop on the Future of Software Engineering Research. ACM, New York (to appear, 2010)"},{"key":"2_CR13","volume-title":"Using MPI: portable parallel programming with the Message-Passing Interface","author":"W. Gropp","year":"1999","unstructured":"Gropp, W., Lusk, E., Skjellum, A.: Using MPI: portable parallel programming with the Message-Passing Interface. MIT Press, Cambridge (1999)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Intl. J. on Software Tools for Technology Transfer 2(4) (April 2000)","DOI":"10.1007\/s100090050043"},{"key":"2_CR15","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall Intl., Englewood Cliffs (1985)"},{"key":"2_CR16","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":"2_CR17","doi-asserted-by":"crossref","unstructured":"Humphrey, A., Derrick, C., Gopalakrishnan, G., Tibbitts, B.R.: GEM: Graphical explorer for MPI programs. In: Parallel Software Tools and Tool Infrastructures, ICPP Workshop (2010), \n                  \n                    http:\/\/www.cs.utah.edu\/fv\/GEM","DOI":"10.1109\/ICPPW.2010.33"},{"key":"2_CR18","unstructured":"Jones, G., Goldsmith, M.: Programming in occam2. Prentice Hall Intl. Series in Computer Science (1988), \n                  \n                    http:\/\/www.comlab.ox.ac.uk\/geraint.jones\/publications\/book\/Pio2\/"},{"issue":"7","key":"2_CR19","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Comm. ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Comm. ACM"},{"issue":"7","key":"2_CR20","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","year":"2008","unstructured":"Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.): EuroPVM\/MPI 2008. LNCS, vol.\u00a05205. Springer, Heidelberg (2008)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Li, G., Palmer, R., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API. Science of Computer Programming (2010), \n                  \n                    http:\/\/dx.doi.org\/10.1016\/j.scico.2010.03.007","DOI":"10.1016\/j.scico.2010.03.007"},{"key":"2_CR23","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.S. Matlin","year":"2002","unstructured":"Matlin, O.S., 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)"},{"key":"2_CR24","unstructured":"Mattson, T., Wijngaart, R.V.: The 48-core SCC processor: the programmers view. In: SC10 [30] (to appear)"},{"key":"2_CR25","unstructured":"Multicore association, \n                  \n                    http:\/\/www.multicore-association.org"},{"key":"2_CR26","unstructured":"Message Passing Interface Forum: MPI: A Message-Passing Interface Standard, version 2.2, September 4, (2009), \n                  \n                    http:\/\/www.mpi-forum.org\/docs\/"},{"key":"2_CR27","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"key":"2_CR28","unstructured":"The Eclipse Parallel Tools Platform, \n                  \n                    http:\/\/www.eclipse.org\/ptp"},{"key":"2_CR29","unstructured":"Research, M.: CHESS: Find and reproduce Heisenbugs in concurrent programs, \n                  \n                    http:\/\/research.microsoft.com\/en-us\/projects\/chess\n                  \n                  \n                 (accessed 11\/7\/10)"},{"key":"2_CR30","unstructured":"SC 2010: The International Conference for High Performance Computing, Networking, Storage and Analysis, New Orleans, LA. ACM, New York (to appear, 2010)"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Schulz, M., de\u00a0Supinski, B.R.: P\n                  N\n                MPI tools: a whole lot greater than the sum of their parts. In: Proceedings of the 2007 ACM\/IEEE Conference on Supercomputing, SC 2007, pp. 30:1\u201330:10. ACM, New York (2007)","DOI":"10.1145\/1362622.1362663"},{"key":"2_CR32","first-page":"41","volume-title":"9th International Conference Formal Methods in Computer Aided Design (FMCAD)","author":"S. Sharma","year":"2009","unstructured":"Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC - A runtime verification tool for MCAPI user applications. In: 9th International Conference Formal Methods in Computer Aided Design (FMCAD), pp. 41\u201344. IEEE, Los Alamitos (2009)"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Sharma, S., Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M., Thakur, R., Gropp, W.: A formal approach to detect functionally irrelevant barriers in MPI programs. In: Lastovetsky et\u00a0al. [21], pp. 265\u2013273","DOI":"10.1007\/978-3-540-87475-1_36"},{"key":"2_CR34","unstructured":"Siegel, S.F.: The Toolkit for Accurate Scientific Software web page (2010), \n                  \n                    http:\/\/vsl.cis.udel.edu\/tass"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-30579-8_27","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. 413\u2013429. Springer, Heidelberg (2005)"},{"key":"2_CR36","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":"2_CR37","doi-asserted-by":"crossref","unstructured":"Siegel, S.F.: Verifying parallel programs with MPI-Spin In: Cappello et al. [6], pp. 13\u201314","DOI":"10.1007\/978-3-540-75416-9_8"},{"key":"2_CR38","unstructured":"Siegel, S.F.: MPI-Spin web page (2008), \n                  \n                    http:\/\/vsl.cis.udel.edu\/mpi-spin"},{"key":"2_CR39","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)"},{"key":"2_CR40","first-page":"95","volume-title":"Proceedings of the 2005 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2005)","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 2005), pp. 95\u2013106. ACM Press, New York (2005)"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Avrunin, G.S.: Verification of halting properties for MPI programs using nonblocking operations. In: Cappello et al. [6], pp. 326\u2013334","DOI":"10.1007\/978-3-540-75416-9_44"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Combining symbolic execution with model checking to verify parallel numerical programs. ACM Transactions on Software Engineering and Methodology\u00a017, Article 10, 1\u201334 (2008)","DOI":"10.1145\/1348250.1348256"},{"key":"2_CR43","unstructured":"Siegel, S.F., Rossi, L.F.: Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In: Lastovetsky et\u00a0al. [21]"},{"key":"2_CR44","series-title":"LNCS","volume-title":"VMCAI 2011","author":"S.F. Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: Collective assertions. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, Springer, Heidelberg (2011)"},{"key":"2_CR45","volume-title":"Proceedings of the 2011 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2011)","author":"S.F. Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: Automatic formal verification of MPI-based parallel programs. In: Proceedings of the 2011 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2011). ACM Press, New York (to appear, 2011)"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Sutter, H.: The free lunch is over: A fundamental turn toward concurrency in software. Dr. Dobb\u2019s Journal 30(3) (March 2005), \n                  \n                    http:\/\/www.drdobbs.com\/architecture-and-design\/184405990","DOI":"10.1145\/1095408.1095421"},{"key":"2_CR47","unstructured":"Vakkalanka, S.: Efficient Dynamic Verification Algorithms for MPI Applications. Ph.D. thesis, University of Utah (2010), \n                  \n                    http:\/\/www.cs.utah.edu\/formal_verification\/pdf\/sarvani_dissertation.pdf"},{"key":"2_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-70545-1_9","volume-title":"Computer Aided Verification","author":"S. Vakkalanka","year":"2008","unstructured":"Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M.: Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 66\u201379. Springer, Heidelberg (2008)"},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-15646-5_16","volume-title":"Recent Advances in the Message Passing Interface","author":"S. Vakkalanka","year":"2010","unstructured":"Vakkalanka, S., Vo, A., Gopalakrishnan, G., Kirby, R.: Precise dynamic analysis for slack elasticity: Adding buffering without adding bugs. In: Keller, R., Gabriel, E., Resch, M., Dongarra, J. (eds.) EuroMPI 2010. LNCS, vol.\u00a06305, pp. 152\u2013159. Springer, Heidelberg (2010)"},{"key":"2_CR50","unstructured":"Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., de Supinski, B.R., Schulz, M., Bronevetsky, G.: A scalable and distributed dynamic formal verifier for MPI programs. In: SC10 [30] (to appear), \n                  \n                    http:\/\/www.cs.utah.edu\/fv\/DAMPI\/sc10.pdf"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. In: PPoPP, pp. 261\u2013269 (2009)","DOI":"10.1145\/1594835.1504214"},{"key":"2_CR52","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/1147403.1147409","volume-title":"PADTAD 2006: Proceeding of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging","author":"R. Vuduc","year":"2006","unstructured":"Vuduc, R., Schulz, M., Quinlan, D., de Supinski, B., S\u00e6bj\u00f8rnsen, A.: Improving distributed memory applications testing by message perturbation. In: PADTAD 2006: Proceeding of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging, pp. 27\u201336. ACM, New York (2006)"},{"key":"2_CR53","first-page":"194","volume-title":"Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2007","author":"Y. Zhang","year":"2007","unstructured":"Zhang, Y., Duesterwald, E.: Barrier matching for programs with textually unaligned barriers. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2007, pp. 194\u2013204. ACM, New York (2007)"}],"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-642-18275-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T21:54:46Z","timestamp":1578520486000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_2"}},"subtitle":["(Invited Talk)"],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}