{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:21:23Z","timestamp":1759033283250,"version":"3.37.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2016,10,28]],"date-time":"2016-10-28T00:00:00Z","timestamp":1477612800000},"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":["Int J Parallel Prog"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10766-016-0467-9","type":"journal-article","created":{"date-parts":[[2016,10,28]],"date-time":"2016-10-28T06:36:24Z","timestamp":1477636584000},"page":"1326-1365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Synchronization Validation for Cross-Thread Dependences in Parallel Programs"],"prefix":"10.1007","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9327-9677","authenticated-orcid":false,"given":"Sudakshina","family":"Dutta","sequence":"first","affiliation":[]},{"given":"Dipankar","family":"Sarkar","sequence":"additional","affiliation":[]},{"given":"Arvind","family":"Rawat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,28]]},"reference":[{"issue":"5","key":"467_CR1","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976). doi:\n                        10.1145\/360051.360224","journal-title":"Commun. ACM"},{"key":"467_CR2","unstructured":"Sinha, A., Malik, S., Gupta, A.: Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. In: FMCAD\u201912, pp. 6\u201315 (2012)"},{"key":"467_CR3","doi-asserted-by":"publisher","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: Proceedings of the 2nd World Congress on Formal Methods, pp. 256\u2013272. Berlin, Heidelberg (2009). ISBN 978-3-642-05088-6. doi:\n                        10.1007\/978-3-642-05089-3_17","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"467_CR4","doi-asserted-by":"publisher","unstructured":"Sethi, D., Talupur, M., Malik, S.: Model checking software. In: Proceedings of 20th International Symposium, Spin 2013, Stony Brook, NY, USA, July 8\u20139, 2013 (2013). doi:\n                        10.1007\/978-3-642-39176-7_20","DOI":"10.1007\/978-3-642-39176-7_20"},{"issue":"3","key":"467_CR5","doi-asserted-by":"crossref","first-page":"556","DOI":"10.1109\/TCAD.2007.913390","volume":"27","author":"C Karfa","year":"2008","unstructured":"Karfa, C., Sarkar, D., Mandal, C., Kumar, P.: An equivalence-checking method for scheduling verification in high-level synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(3), 556\u2013569 (2008). ISSN 0278-0070","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"4","key":"467_CR6","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1109\/TCAD.2010.2042889","volume":"29","author":"S Kundu","year":"2010","unstructured":"Kundu, S., Lerner, S., Gupta, R.K.: Translation validation of high-level synthesis. IEEE Trans. CAD Integr. Circuits Syst. 29(4), 566\u2013579 (2010). doi:\n                        10.1109\/TCAD.2010.2042889","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"467_CR7","doi-asserted-by":"publisher","unstructured":"Bandyopadhyay, S., Banerjee, K., Sarkar, D., Mandal, C.: Translation validation for PRES+ models of parallel behaviours via an FSMD equivalence checker. In: Proceedings of Progress in VLSI Design and Test\u201416th International Symposium, VDAT 2012, Shibpur, India, July 1\u20134, 2012, pp. 69\u201378 (2012). doi:\n                        10.1007\/978-3-642-31494-0_9","DOI":"10.1007\/978-3-642-31494-0_9"},{"key":"467_CR8","unstructured":"Hu, L., Hutton, G.: Compiling concurrency correctly: cutting out the middle man. In: Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Kom\u00e1rno, Slovakia, June 2\u20134, 2009, pp. 17\u201332 (2009)"},{"issue":"7","key":"467_CR9","doi-asserted-by":"publisher","first-page":"710","DOI":"10.1109\/TSE.2013.2297120","volume":"40","author":"P Collingbourne","year":"2014","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of data-parallel floating-point code. IEEE Trans. Softw. Eng. 40(7), 710\u2013737 (2014). doi:\n                        10.1109\/TSE.2013.2297120","journal-title":"IEEE Trans. Softw. Eng."},{"key":"467_CR10","doi-asserted-by":"publisher","unstructured":"Nicolau, A., Li, G., Kejariwal, A.: Techniques for efficient placement of synchronization primitives. In: Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP\u201909, pp. 199\u2013208. ACM, New York, NY, USA (2009). ISBN 978-1-60558-397-6. doi:\n                        10.1145\/1504176.1504207","DOI":"10.1145\/1504176.1504207"},{"key":"467_CR11","unstructured":"Kahlon, V.: Automatic lock insertion in concurrent programs. In: Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22\u201325, 2012, pp. 16\u201323 (2012). \n                        http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp?arnumber=6462551"},{"key":"467_CR12","doi-asserted-by":"crossref","unstructured":"Dutta, S., Sarkar, D., Rawat, A., Singh, K.: Validation of loop parallelization and loop vectorization transformations. In: Proceedings of Evaluation of Novel Software Approaches to Software Engineering (to appear) (2016)","DOI":"10.5220\/0005869501950202"},{"issue":"1","key":"467_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF01407931","volume":"20","author":"P Feautrier","year":"1991","unstructured":"Feautrier, P.: Dataflow analysis of array and scalar references. Int. J. Parallel Program. 20(1), 23\u201353 (1991). doi:\n                        10.1007\/BF01407931","journal-title":"Int. J. Parallel Program."},{"key":"467_CR14","unstructured":"Liang, D., Harrold, M.J.: Slicing objects using system dependence graphs. In: Proceedings of the International Conference on Software Maintenance, ICSM\u201998, p. 358. IEEE Computer Society, Washington, DC, USA (1998). ISBN 0-8186-8779-7. \n                        http:\/\/dl.acm.org\/citation.cfm?id=850947.853342"},{"key":"467_CR15","doi-asserted-by":"publisher","unstructured":"Collard, J., Barthou, D., Feautrier, P.: Fuzzy array dataflow analysis. In: Proceedings of the Fifth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP\u201995, pp. 92\u2013101. ACM, New York, NY, USA (1995). ISBN 0-89791-700-6. doi:\n                        10.1145\/209936.209947","DOI":"10.1145\/209936.209947"},{"key":"467_CR16","doi-asserted-by":"publisher","unstructured":"Krinke, J.: Static slicing of threaded programs. In: Proceedings of the 1998 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE\u201998, pp. 35\u201342. ACM, New York, NY, USA (1998). ISBN 1-58113-055-4. doi:\n                        10.1145\/277631.277638","DOI":"10.1145\/277631.277638"},{"key":"467_CR17","doi-asserted-by":"publisher","unstructured":"Cheng, J.: Process dependence net of distributed programs and its applications in development of distributed systems. In: Computer Software and Applications Conference, 1993. COMPSAC 93. Proceedings., Seventeenth Annual International, pp. 231\u2013240 (1993). doi:\n                        10.1109\/CMPSAC.1993.404187","DOI":"10.1109\/CMPSAC.1993.404187"},{"issue":"5\u20136","key":"467_CR18","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1147\/rd.355.0779","volume":"35","author":"V Sarkar","year":"1991","unstructured":"Sarkar, V.: Automatic partitioning of a program dependence graph into parallel tasks. IBM J. Res. Dev. 35(5\u20136), 779\u2013804 (1991). doi:\n                        10.1147\/rd.355.0779","journal-title":"IBM J. Res. Dev."},{"issue":"3","key":"467_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319\u2013349 (1987). doi:\n                        10.1145\/24039.24041","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"467_CR20","doi-asserted-by":"publisher","unstructured":"Allen, J.R., Kennedy, K., Porterfield, C., Warren, J.: Conversion of control dependence to data dependence. In: Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL\u201983, pp. 177\u2013189. ACM, New York, NY, USA (1983). ISBN 0-89791-090-7. doi:\n                        10.1145\/567067.567085","DOI":"10.1145\/567067.567085"},{"key":"467_CR21","doi-asserted-by":"crossref","first-page":"1310","DOI":"10.1109\/DATE.2005.163","volume":"2","author":"KC Shashidhar","year":"2005","unstructured":"Shashidhar, K.C., Bruynooghe, M., Catthoor, F., Janssens, G.: Functional equivalence checking for verification of algebraic transformations on array-intensive source code. Proc. Des. Autom. Test Eur. 2, 1310\u20131315 (2005)","journal-title":"Proc. Des. Autom. Test Eur."},{"issue":"11","key":"467_CR22","doi-asserted-by":"crossref","first-page":"1787","DOI":"10.1109\/TCAD.2013.2272536","volume":"32","author":"C Karfa","year":"2013","unstructured":"Karfa, C., Banerjee, K., Sarkar, D., Mandal, C.: Verification of loop and arithmetic transformations of array-intensive behaviors. IEEE Trans. CAD Integr. Circuits Syst. 32(11), 1787\u20131800 (2013)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"issue":"3","key":"467_CR23","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/2362389.2362390","volume":"34","author":"S Verdoolaege","year":"2012","unstructured":"Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3), 11:1\u201311:35 (2012). doi:\n                        10.1145\/2362389.2362390","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"02","key":"467_CR24","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1142\/S0129626497000140","volume":"07","author":"J-F Collard","year":"1997","unstructured":"Collard, J.-F., Griebl, M.: Array dataflow analysis for explicitly parallel programs. Parallel Process. Lett. 07(02), 117\u2013131 (1997). doi:\n                        10.1142\/S0129626497000140","journal-title":"Parallel Process. Lett."},{"key":"467_CR25","first-page":"9","volume":"2","author":"SP Midkiff","year":"1991","unstructured":"Midkiff, S.P., Padua, D.A.: A comparison of four synchronization optimization techniques. ICPP 2, 9\u201316 (1991)","journal-title":"ICPP"},{"key":"467_CR26","unstructured":"Griebl, M., Lengauer, C.: The loop parallelizer loopo. In: Proceedings of Sixth Workshop on Compilers for Parallel Computers, volume 21 of Konferenzen des Forschungszentrums J\u00fclich, pp. 311\u2013320. Forschungszentrum (1996)"},{"key":"467_CR27","doi-asserted-by":"crossref","unstructured":"Bondhugula, U., Baskaran, M., Krishnamoorthy, S., Ramanujam, J., Rountev, A., Sadayappan, P.: Automatic transformations for communication-minimized parallelization and locality optimization in the polyhedral model. In: International Conference on Compiler Construction (ETAPS CC) (2008)","DOI":"10.1007\/978-3-540-78791-4_9"},{"key":"467_CR28","unstructured":"Amini, M., Goubier, O., Guelton, S., McMahon, J.O., Pasquier, F., P\u00e9an, G., Villalon, P.: Par4all: from convex array regions to heterogeneous computing. In: IMPACT 2012: Second International Workshop on Polyhedral Compilation Techniques HiPEAC 2012 (2012)"}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-016-0467-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-016-0467-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-016-0467-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,21]],"date-time":"2017-09-21T02:35:21Z","timestamp":1505961321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-016-0467-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,28]]},"references-count":28,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["467"],"URL":"https:\/\/doi.org\/10.1007\/s10766-016-0467-9","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"type":"print","value":"0885-7458"},{"type":"electronic","value":"1573-7640"}],"subject":[],"published":{"date-parts":[[2016,10,28]]}}}