{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:56:52Z","timestamp":1756000612217},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_19","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"263-278","source":"Crossref","is-referenced-by-count":23,"title":["Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs"],"prefix":"10.1007","author":[{"given":"Vojt\u011bch","family":"Forejt","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Ganesh","family":"Narayanaswamy","sequence":"additional","affiliation":[]},{"given":"Subodh","family":"Sharma","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 141\u2013157. Springer, Heidelberg (2013)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Carter, J.D., Gardner, W.B., Grewal, G.: The Pilot library for novice MPI programmers. In: PPoPP, pp. 351\u2013352. ACM (2010)","DOI":"10.1145\/1837853.1693509"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Chen, F., Serbanuta, T.F., Rosu, G.: jPredictor: A predictive runtime analysis tool for Java. In: ICSE, pp. 221\u2013230. ACM (2008)","DOI":"10.1145\/1368088.1368119"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"3","key":"19_CR5","first-page":"23","volume":"17","author":"E. Deniz","year":"2012","unstructured":"Deniz, E., Sen, A., Holt, J.: Verification and coverage of message passing multicore applications. ACM Trans. Design Autom. Electr. Syst.\u00a017(3), 23 (2012)","journal-title":"ACM Trans. Design Autom. Electr. Syst."},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Elwakil, M., Yang, Z.: Debugging support tool for MCAPI applications. In: PDATAD, pp. 20\u201325. ACM (2010)","DOI":"10.1145\/1866210.1866212"},{"issue":"8","key":"19_CR8","doi-asserted-by":"publisher","first-page":"1397","DOI":"10.1016\/j.jcss.2006.03.003","volume":"72","author":"S. Gradara","year":"2006","unstructured":"Gradara, S., Santone, A., Villani, M.L.: DELFIN\u2009+\u2009: An efficient deadlock detection tool for CCS processes. J. Comput. Syst. Sci.\u00a072(8), 1397\u20131412 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Gropp, W., Lusk, E., Skjellum, A.: Using MPI. MIT Press (1999)","DOI":"10.7551\/mitpress\/7056.001.0001"},{"issue":"1","key":"19_CR10","first-page":"19","volume":"28","author":"W. Haque","year":"2006","unstructured":"Haque, W.: Concurrent deadlock detection in parallel programs. Int. J. Comput. Appl.\u00a028(1), 19\u201325 (2006)","journal-title":"Int. J. Comput. Appl."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Hilbrich, T., Protze, J., Schulz, M., de Supinski, B.R., M\u00fcller, M.S.: MPI runtime error detection with MUST: advances in deadlock detection. In: SC, p. 30 (2012)","DOI":"10.1109\/SC.2012.79"},{"issue":"3","key":"19_CR12","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/MM.2009.48","volume":"29","author":"J. Holt","year":"2009","unstructured":"Holt, J., Agarwal, A., Brehmer, S., Domeika, M., Griffin, P., Schirrmeister, F.: Software standards for the multicore era. IEEE Micro\u00a029(3), 40\u201351 (2009)","journal-title":"IEEE Micro"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Huang, Y., Mercer, E., McCarthy, J.: Proving MCAPI executions are correct using SMT. In: ASE, pp. 26\u201336. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693063"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Krammer, B., Bidmon, K., M\u00fcller, M.S., Resch, M.M.: MARMOT: An MPI analysis and checking tool. In: PARCO. Advances in Parallel Computing, vol.\u00a013, pp. 493\u2013500. Elsevier (2003)","DOI":"10.1016\/S0927-5452(04)80063-7"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Leung, A., Gupta, M., Agarwal, Y., Gupta, R., Jhala, R., Lerner, S.: Verifying GPU kernels by test amplification. In: PLDI, pp. 383\u2013394. ACM (2012)","DOI":"10.1145\/2345156.2254110"},{"issue":"11","key":"19_CR16","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1002\/cpe.701","volume":"14","author":"G.R. Luecke","year":"2002","unstructured":"Luecke, G.R., Zou, Y., Coyle, J., Hoekstra, J., Kraeva, M.: Deadlock detection in MPI programs. Concurrency and Computation: Practice and Experience\u00a014(11), 911\u2013932 (2002)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"19_CR17","unstructured":"Message Passing Interface, \n                  \n                    http:\/\/www.mpi-forum.org\/docs\/mpi-2.2"},{"key":"19_CR18","unstructured":"Mueller, M.S., Gopalakrishnan, G., de Supinski, B.R., Lecomber, D., Hilbrich, T.: Dealing with MPI bugs at scale: Best practices, automatic detection, debugging, and formal verification, \n                  \n                    http:\/\/sc11.supercomputing.org\/schedule\/event_detail.php?evid=tut131"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-13883-8_68","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"N. Natarajan","year":"1984","unstructured":"Natarajan, N.: A distributed algorithm for detecting communication deadlocks. In: Joseph, M., Shyamasundar, R.K. (eds.) FSTTCS 1984. LNCS, vol.\u00a0181, pp. 119\u2013135. Springer, Heidelberg (1984)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC: A runtime verification tool for MCAPI user applications. In: FMCAD, pp. 41\u201344 (2009)","DOI":"10.1109\/FMCAD.2009.5351145"},{"key":"19_CR21","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)"},{"issue":"4","key":"19_CR22","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s11786-011-0101-6","volume":"5","author":"S.F. Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: FEVS: A functional equivalence verification suite for high-performance scientific computing. Mathematics in Computer Science\u00a05(4), 427\u2013435 (2011)","journal-title":"Mathematics in Computer Science"},{"key":"19_CR23","unstructured":"Siegel, S.F., Zirkel, T.K.: The Toolkit for Accurate Scientific Software. Technical Report UDEL-CIS-2011\/01, Department of Computer and Information Sciences, University of Delaware (2011)"},{"key":"19_CR24","unstructured":"Vakkalanka, S.: Efficient dynamic verification algorithms for MPI applications. PhD thesis, University of Utah, Salt Lake City, UT, USA, AAI3413092 (2010)"},{"key":"19_CR25","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":"19_CR26","doi-asserted-by":"crossref","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: SC, pp. 1\u201310. IEEE (2010)","DOI":"10.1109\/SC.2010.7"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-05089-3_17","volume-title":"FM 2009: Formal Methods","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 256\u2013272. Springer, Heidelberg (2009)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Xue, R., Liu, X., Wu, M., Guo, Z., Chen, W., Zheng, W., Zhang, Z., Voelker, G.: MPIWiz: subgroup reproducible replay of MPI applications. In: PPoPP, pp. 251\u2013260. ACM (2009)","DOI":"10.1145\/1594835.1504213"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T16:33:14Z","timestamp":1558888394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}