{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:34:03Z","timestamp":1752986043840,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,1,6]],"date-time":"2018-01-06T00:00:00Z","timestamp":1515196800000},"content-version":"tdm","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":[[2019,2]]},"DOI":"10.1007\/s10766-017-0548-4","type":"journal-article","created":{"date-parts":[[2018,1,6]],"date-time":"2018-01-06T07:18:44Z","timestamp":1515223124000},"page":"59-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verifying Parallel Code After Refactoring Using Equivalence Checking"],"prefix":"10.1007","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2605-4272","authenticated-orcid":false,"given":"Moria","family":"Abadi","sequence":"first","affiliation":[]},{"given":"Sharon","family":"Keidar-Barner","sequence":"additional","affiliation":[]},{"given":"Dmitry","family":"Pidan","sequence":"additional","affiliation":[]},{"given":"Tatyana","family":"Veksler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,1,6]]},"reference":[{"key":"548_CR1","doi-asserted-by":"crossref","unstructured":"Parkhurst, J., Darringer, J., Grundmann, B.: From single core to multi-core: preparing for a new exponential. In: Proceedings of the 2006 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD\u201906, pp. 67\u201372. ACM, New York (2006)","DOI":"10.1145\/1233501.1233516"},{"issue":"3","key":"548_CR2","first-page":"202","volume":"30","author":"H Sutter","year":"2005","unstructured":"Sutter, H.: The free lunch is over: a fundamental turn toward concurrency in software. Dr. Dobb\u2019s J. 30(3), 202\u2013210 (2005)","journal-title":"Dr. Dobb\u2019s J."},{"key":"548_CR3","doi-asserted-by":"crossref","unstructured":"Dig, D., Marrero, J., Ernst, M.D.: Refactoring sequential Java code for concurrency via concurrent libraries. In: Proceedings of the 31st International Conference on Software Engineering, ICSE\u201909, pp. 397\u2013407. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/ICSE.2009.5070539"},{"key":"548_CR4","unstructured":"Aldinucci, M., Torquati, M., Meneghin, M.: Fastflow: efficient parallel streaming applications on multi-core. CORR (2009). arXiv:0909.1187"},{"key":"548_CR5","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-79561-2_15","volume-title":"OpenMP in a New Era of Parallelism. Lecture Notes in Computer Science","author":"F Broquedis","year":"2008","unstructured":"Broquedis, F., Diakhat\u00e9, F., Thibault, S., Aumage, O., Namyst, R., Wacrenier, P.-A.: Scheduling dynamic openMP applications over multicore architectures. In: Eigenmann, R., Supinski, B. (eds.) OpenMP in a New Era of Parallelism. Lecture Notes in Computer Science, vol. 5004, pp. 170\u2013180. Springer, Berlin (2008)"},{"key":"548_CR6","doi-asserted-by":"crossref","unstructured":"Lea, D.: A Java fork\/join framework. In: Proceedings of the ACM 2000 Conference on Java Grande, JAVA\u201900, pp. 36\u201343. ACM, New York (2000)","DOI":"10.1145\/337449.337465"},{"issue":"4","key":"548_CR7","first-page":"298","volume":"23","author":"C Pheatt","year":"2008","unstructured":"Pheatt, C.: Intel $${}^{\\textregistered }$$ \u00ae threading building blocks. J. Comput. Sci. Coll. 23(4), 298\u2013298 (2008)","journal-title":"J. Comput. Sci. Coll."},{"key":"548_CR8","doi-asserted-by":"crossref","unstructured":"Janjic, V., Brown, C., Mackenzie, K., Hammond, K., Danelutto, M., Aldinucci, M., Garcia, J.D.: RPL: a domain-specific language for designing and implementing parallel C++ applications. In: 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), pp. 288\u2013295. IEEE (2016)","DOI":"10.1109\/PDP.2016.122"},{"key":"548_CR9","doi-asserted-by":"crossref","unstructured":"Chen, F., Yang, H., Chu, W.C.C., Xu, B.: A program transformation framework for multicore software reengineering. In: 2012 12th International Conference on Quality Software, pp. 270\u2013275 (Aug. 2012)","DOI":"10.1109\/QSIC.2012.46"},{"key":"548_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: ACM Sigplan Notices, vol. 40, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"548_CR11","doi-asserted-by":"publisher","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball T., Jones R.B. (eds.) Computer Aided Verification (CAV), pp. 419\u2013423. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/11817963_38","DOI":"10.1007\/11817963_38"},{"key":"548_CR12","doi-asserted-by":"crossref","unstructured":"Cadar, C., Godefroid, P., Khurshid, S., P\u0103s\u0103reanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 1066\u20131071. ACM (2011)","DOI":"10.1145\/1985793.1985995"},{"issue":"4","key":"548_CR13","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"CS P\u0103s\u0103reanu","year":"2009","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. 11(4), 339\u2013353 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"548_CR14","first-page":"209","volume":"8","author":"C Cadar","year":"2008","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI 8, 209\u2013224 (2008)","journal-title":"OSDI"},{"key":"548_CR15","doi-asserted-by":"crossref","unstructured":"Barner, S., Eisner, C., Glazberg, Z., Kroening, D., Rabinovitz, I.: ExpliSAT: guiding SAT-based software verification with explicit states. In: Hardware and Software, Verification and Testing, pp. 138\u2013154. Springer (2007)","DOI":"10.1007\/978-3-540-70889-6_11"},{"key":"548_CR16","doi-asserted-by":"crossref","unstructured":"Chockler, H., Pidan, D., Ruah, S.: Improving representative computation in ExpliSAT. In: Hardware and Software: Verification and Testing, pp. 359\u2013364. Springer (2013)","DOI":"10.1007\/978-3-319-03077-7_24"},{"key":"548_CR17","unstructured":"Torquati, M.: Single-producer\/single-consumer queues on shared cache multi-core systems. CoRR (2010). arXiv:1012.1824"},{"key":"548_CR18","unstructured":"The mandelbrot set in C++11. http:\/\/solarianprogrammer.com\/2013\/02\/28\/mandelbroot-set-cpp-11"},{"key":"548_CR19","unstructured":"Escape time algorithm. https:\/\/en.wikipedia.org\/wiki\/Mandelbrot_set#Escape_time_algorithm"},{"key":"548_CR20","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Elspas, B., Levitt, K.N.: Select\u2014a formal system for testing and debugging programs by symbolic execution. In: Proceedings of the International Conference on Reliable Software, pp. 234\u2013245","DOI":"10.1145\/800027.808445"},{"issue":"7","key":"548_CR21","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"548_CR22","doi-asserted-by":"crossref","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 119\u2013135. Springer (2012)","DOI":"10.1007\/978-3-642-27940-9_9"},{"key":"548_CR23","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: Piterman N., Smolka S.A. (eds.) 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 292\u2013307. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_21"},{"key":"548_CR24","doi-asserted-by":"crossref","unstructured":"Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: an industrial experience report. In: International Conference on Integrated Formal Methods, pp. 311\u2013325. Springer (2016)","DOI":"10.1007\/978-3-319-33693-0_20"},{"key":"548_CR25","doi-asserted-by":"crossref","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J., Stappers, F.P., de Vink, E.P., Wesselink, W., Willemse, T.A.: An overview of the mCRL2 toolset and its recent advances. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 199\u2013213. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"548_CR26","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Proceedings of the 2006 International Symposium on Software Testing and Analysis, pp. 157\u2013168. ACM (2006)","DOI":"10.1145\/1146238.1146256"},{"issue":"8","key":"548_CR27","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1145\/2038037.1941603","volume":"46","author":"SF Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: Automatic formal verification of MPI-based parallel programs. SIGPLAN Not. 46(8), 309\u2013310 (2011)","journal-title":"SIGPLAN Not."}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-017-0548-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-017-0548-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-017-0548-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T22:51:53Z","timestamp":1570575113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-017-0548-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,6]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["548"],"URL":"https:\/\/doi.org\/10.1007\/s10766-017-0548-4","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"type":"print","value":"0885-7458"},{"type":"electronic","value":"1573-7640"}],"subject":[],"published":{"date-parts":[[2018,1,6]]},"assertion":[{"value":"30 May 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 January 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}