{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:28:59Z","timestamp":1746289739867,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319955810"},{"type":"electronic","value":"9783319955827"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-95582-7_28","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T10:31:17Z","timestamp":1531305077000},"page":"466-484","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Dynamic Symbolic Verification of MPI Programs"],"prefix":"10.1007","author":[{"given":"Dhriti","family":"Khanna","sequence":"first","affiliation":[]},{"given":"Subodh","family":"Sharma","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Rodr\u00edguez","sequence":"additional","affiliation":[]},{"given":"Rahul","family":"Purandare","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"28_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. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-48989-6_7","volume-title":"FM 2016: Formal Methods","author":"S B\u00f6hm","year":"2016","unstructured":"B\u00f6hm, S., Meca, O., Jan\u010dar, P.: State-space reduction of non-deterministically synchronizing systems applicable to deadlock detection in MPI. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 102\u2013118. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_7"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the Sixth Conference on Computer Systems. EuroSys 2011, pp. 183\u2013198. ACM (2011)","DOI":"10.1145\/1966445.1966463"},{"key":"28_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI 2008, pp. 209\u2013224. USENIX Association (2008)"},{"key":"28_CR5","unstructured":"Clang: A C language family frontend for LLVM. http:\/\/clang.llvm.org\/"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-15643-4_27","volume-title":"Automated Technology for Verification and Analysis","author":"Mohamed Elwakil","year":"2010","unstructured":"Elwakil, Mohamed, Yang, Zijiang, Wang, Liqiang: CRI: symbolic debugger for MCAPI applications. In: Bouajjani, Ahmed, Chin, Wei-Ngan (eds.) ATVA 2010. LNCS, vol. 6252, pp. 353\u2013358. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_27"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Eslamimehr, M., Palsberg, J.: Sherlock: scalable deadlock detection for concurrent programs. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. FSE 2014, pp. 353\u2013365. ACM (2014)","DOI":"10.1145\/2635868.2635918"},{"issue":"4","key":"28_CR9","doi-asserted-by":"publisher","first-page":"15:1","DOI":"10.1145\/3095075","volume":"39","author":"V Forejt","year":"2017","unstructured":"Forejt, V., Joshi, S., Kroening, D., Narayanaswamy, G., Sharma, S.: Precise predictive analysis for discovering communication deadlocks in MPI programs. ACM Trans. Program. Lang. Syst. 39(4), 15:1\u201315:27 (2017)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-06410-9_19","volume-title":"FM 2014: Formal Methods","author":"V Forejt","year":"2014","unstructured":"Forejt, V., Kroening, D., Narayanaswamy, G., Sharma, S.: Precise predictive analysis for discovering communication deadlocks in MPI programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 263\u2013278. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_19"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Fu, X., Chen, Z., Yu, H., Huang, C., Dong, W., Wang, J.: Symbolic execution of MPI programs. In: Proceedings of the 37th International Conference on Software Engineering, vol. 2. ICSE 2015, pp. 809\u2013810. IEEE Press (2015)","DOI":"10.1109\/ICSE.2015.259"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Ganai, M., Lee, D., Gupta, A.: DTAM: dynamic taint analysis of multi-threaded programs for relevancy. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. FSE 2012, pp. 46:1\u201346:11 (2012)","DOI":"10.1145\/2393596.2393650"},{"key":"28_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, 2nd edn. MIT Press, Cambridge (1999)","edition":"2"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-17524-9_16","volume-title":"NASA Formal Methods","author":"Y Huang","year":"2015","unstructured":"Huang, Y., Mercer, E.: Detecting MPI zero buffer incompatibility by SMT encoding. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 219\u2013233. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_16"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Huang, Y., Mercer, E., McCarthy, J.: Proving MCAPI executions are correct using SMT. In: Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering, pp. 26\u201336. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693063"},{"key":"28_CR16","first-page":"493","volume-title":"Advances in Parallel Computing","author":"B. Krammer","year":"2004","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. Elsevier (2003)"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"L\u00f3pez, H.A., Marques, E.R.B., Martins, F., Ng, N., Santos, C., Vasconcelos, V.T., Yoshida, N.: Protocol-based verification of message-passing parallel programs. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2015, pp. 280\u2013298. ACM (2015)","DOI":"10.1145\/2814270.2814302"},{"issue":"11","key":"28_CR18","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1002\/cpe.701","volume":"14","author":"GR Luecke","year":"2002","unstructured":"Luecke, G.R., Zou, Y., Coyle, J., Hoekstra, J., Kraeva, M.: Deadlock detection in MPI programs. Concurrency Comput. Pract. Experience 14(11), 911\u2013932 (2002)","journal-title":"Concurrency Comput. Pract. Experience"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Luo, Z., Zheng, M., Siegel, S.F.: Verification of MPI programs using CIVL. In: Proceedings of the 24th European MPI Users\u2019 Group Meeting. EuroMPI 2017, pp. 6:1\u20136:11. ACM (2017)","DOI":"10.1145\/3127024.3127032"},{"key":"28_CR20","doi-asserted-by":"publisher","first-page":"103","DOI":"10.4204\/EPTCS.137.9","volume":"137","author":"Eduardo R. B. Marques","year":"2013","unstructured":"Marques, E.R.B., Martins, F., Vasconcelos, V.T., Ng, N., Martins, N.: Towards deductive verification of MPI programs against session types. In: Proceedings 6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. PLACES 2013, pp. 103\u2013113 (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"28_CR21","unstructured":"MPI: A message-passing interface standard version 3.1. http:\/\/mpi-forum.org\/docs\/mpi-3.1\/"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Narayanaswamy, G.: When truth is efficient: analysing concurrency. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis. ISSTA 2015, pp. 141\u2013152. ACM (2015)","DOI":"10.1145\/2771783.2771790"},{"issue":"8","key":"28_CR23","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/3155284.3018767","volume":"52","author":"Kento Sato","year":"2017","unstructured":"Sato, K., Ahn, D.H., Laguna, I., Lee, G.L., Schulz, M., Chambreau, C.M.: Noise injection techniques to expose subtle and unintended message races. In: Proceedings of the 22Nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP 2017, pp. 89\u2013101 (2017)","journal-title":"ACM SIGPLAN Notices"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for c. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ESEC\/FSE 2013, pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"28_CR25","unstructured":"Sharma, S.V., Gopalakrishnan, G., Kirby, R.M.: A survey of MPI related debuggers and tools. Technical Report UUCS-07-015, University of Utah, School of Computing (2007). http:\/\/www.cs.utah.edu\/research\/techreports.shtml"},{"key":"28_CR26","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":"SF 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. 3385, pp. 413\u2013429. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_27"},{"key":"28_CR27","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s11786-011-0101-6","volume":"5","author":"SF Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: Fevs: a functional equivalence verification suite for high-performance scientific computing. Math. Comput. Sci. 5, 427\u2013435 (2011)","journal-title":"Math. Comput. Sci."},{"issue":"4","key":"28_CR28","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s11786-011-0100-7","volume":"5","author":"SF Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: TASS: the toolkit for accurate scientific software. Math. Comput. Sci. 5(4), 395\u2013426 (2011)","journal-title":"Math. Comput. Sci."},{"key":"28_CR29","unstructured":"Vakkalanka, S.: Efficient Dynamic Verification Algorithms for MPI Applications. Ph.D thesis (2010)"},{"key":"28_CR30","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. 5123, pp. 66\u201379. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_9"},{"key":"28_CR31","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.M.: 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. 6305, pp. 152\u2013159. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15646-5_16"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"Vetter, J.S., de Supinski, B.R.: Dynamic software testing of MPI applications with umpire. In: Proceedings of the 2000 ACM\/IEEE Conference on Supercomputing. SC 2000. IEEE Computer Society (2000)","DOI":"10.1109\/SC.2000.10055"},{"key":"28_CR33","doi-asserted-by":"crossref","unstructured":"Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., Supinski, B.R.D., Schulz, M., Bronevetsky, G.: A scalable and distributed dynamic formal verifier for MPI programs. In: Proceedings of the 2010 ACM\/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis. SC 2010, pp. 1\u201310. IEEE Computer Society (2010)","DOI":"10.1109\/SC.2010.7"},{"key":"28_CR34","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. 5850, pp. 256\u2013272. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_17"},{"key":"28_CR35","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Chao Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010, pp. 328\u2013342 (2010)"},{"issue":"4","key":"28_CR36","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1145\/1594835.1504213","volume":"44","author":"Ruini Xue","year":"2009","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: Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP 2009, pp. 251\u2013260 (2009)","journal-title":"ACM SIGPLAN Notices"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T12:30:43Z","timestamp":1571574643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}