{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T17:08:38Z","timestamp":1748365718806,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030614690"},{"type":"electronic","value":"9783030614706"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-61470-6_8","type":"book-chapter","created":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T18:03:12Z","timestamp":1603735392000},"page":"117-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Safer Parallelization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]},{"given":"Asmae","family":"Heydari Tabar","sequence":"additional","affiliation":[]},{"given":"Arya","family":"Mazaheri","sequence":"additional","affiliation":[]},{"given":"Mohammad","family":"Norouzi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4439-7129","authenticated-orcid":false,"given":"Dominic","family":"Steinh\u00f6fel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6595-3599","authenticated-orcid":false,"given":"Felix","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,27]]},"reference":[{"key":"8_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Boston (1986)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book. LNCS, vol. 10001. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 363\u2013366. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/3-540-46428-X_25"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-319-98047-8_3","volume-title":"Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday","author":"B Beckert","year":"2018","unstructured":"Beckert, B., Ulbrich, M.: Trends in relational program verification. In: M\u00fcller, P., Schaefer, T. (eds.) Principled Software Development, pp. 41\u201358. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-98047-8_3"},{"key":"8_CR6","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. TTCS. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"FM 2014: Formal Methods","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127\u2013131. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-06410-9_9"},{"key":"8_CR8","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364 (2011)"},{"issue":"6","key":"8_CR9","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/390016.808445","volume":"10","author":"RS Boyer","year":"1975","unstructured":"Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT\u2013a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Not. 10(6), 234\u2013245 (1975)","journal-title":"ACM SIGPLAN Not."},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2007.11.015","volume":"199","author":"R Bubel","year":"2008","unstructured":"Bubel, R., Roth, A., R\u00fcmmer, P.: Ensuring the correctness of lightweight tactics for JavaCard dynamic logic. Electr. Notes Theor. Comput. Sci. 199, 107\u2013128 (2008). \nhttps:\/\/doi.org\/10.1016\/j.entcs.2007.11.015","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Dong, J., Sun, Y., Zhao, Y.: Design pattern detection by template matching. In: Wainwright, R.L., Haddad, H. (eds.) Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), pp. 765\u2013769. ACM (2008)","DOI":"10.1145\/1363686.1363864"},{"key":"8_CR12","series-title":"Addison-Wesley Signature Series","volume-title":"Refactoring: Improving the Design of Existing Code","author":"M Fowler","year":"2018","unstructured":"Fowler, M.: Refactoring: Improving the Design of Existing Code. Addison-Wesley Signature Series, 2nd edn. Addison-Wesley Professional, Boston (2018)","edition":"2"},{"key":"8_CR13","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Boston (1995)"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Garrido, A., Meseguer, J.: Formal specification and verification of Java refactorings. In: Proceedings of the 6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006, pp. 165\u2013174. IEEE Computer Society, Washington, D.C. (2006). \nhttps:\/\/doi.org\/10.1109\/SCAM.2006.16","DOI":"10.1109\/SCAM.2006.16"},{"issue":"3","key":"8_CR15","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1002\/stvr.1472","volume":"23","author":"B Godlin","year":"2013","unstructured":"Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23(3), 241\u2013258 (2013). \nhttps:\/\/doi.org\/10.1002\/stvr.1472","journal-title":"Softw. Test. Verif. Reliab."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science: State of the Art and Perspectives","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"issue":"10","key":"8_CR17","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"4","key":"8_CR18","doi-asserted-by":"publisher","first-page":"64:1","DOI":"10.1145\/2688905","volume":"11","author":"ZU Huda","year":"2015","unstructured":"Huda, Z.U., Jannesari, A., Wolf, F.: Using template matching to infer parallel design patterns. TACO 11(4), 64:1\u201364:21 (2015). \nhttps:\/\/doi.org\/10.1145\/2688905","journal-title":"TACO"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Jahr, R., Gerdes, M., Ungerer, T.: A pattern-supported parallelization approach. In: Balaji, P., Guo, M., Huang, Z. (eds.) Proceedings of the 2013 PPOPP International Workshop on Programming Models and Applications for Multicores and Manycores (PMAM), pp. 53\u201362. ACM (2013). \nhttps:\/\/doi.org\/10.1145\/2442992.2442998","DOI":"10.1145\/2442992.2442998"},{"issue":"3","key":"8_CR21","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The Dynamic Frames Theory. Formal Asp. Comput. 23(3), 267\u2013288 (2011). \nhttps:\/\/doi.org\/10.1007\/s00165-010-0152-5","journal-title":"Formal Asp. Comput."},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Khatchadourian, R., Tang, Y., Bagherzadeh, M., Ahmed, S.: Safe automated refactoring for intelligent parallelization of Java 8 streams. In: Atlee, J.M., Bultan, T., Whittle, J. (eds.) Proceedings of the 41st International Conference on Software Engineering (ICSE), pp. 619\u2013630. IEEE\/ACM (2019). \nhttps:\/\/doi.org\/10.1109\/ICSE.2019.00072","DOI":"10.1109\/ICSE.2019.00072"},{"issue":"7","key":"8_CR23","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":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Proceedings of the PLDI 2009, pp. 327\u2013337 (2009)","DOI":"10.1145\/1543135.1542513"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Li, Z., Jannesari, A., Wolf, F.: Discovery of potential parallelism in sequential programs. In: 42nd International Conference on Parallel Processing, ICPP, pp. 1004\u20131013. IEEE Computer Society (2013)","DOI":"10.1109\/ICPP.2013.119"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Li, Z., Jannesari, A., Wolf, F.: An efficient data-dependence profiler for sequential and parallel programs. In: Proceedings of the 29th IEEE International Parallel and Distributed Processing Symposium (IPDPS), Hyderabad, India, pp. 484\u2013493. IEEE Computer Society, May 2015. \nhttps:\/\/doi.org\/10.1109\/IPDPS.2015.41","DOI":"10.1109\/IPDPS.2015.41"},{"issue":"2","key":"8_CR29","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3166064","volume":"61","author":"NP Lopes","year":"2018","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Practical verification of peephole optimizations with alive. Commun. ACM 61(2), 84\u201391 (2018)","journal-title":"Commun. ACM"},{"issue":"2","key":"8_CR30","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s100090100045","volume":"3","author":"BL Massingill","year":"2001","unstructured":"Massingill, B.L., Mattson, T.G., Sanders, B.A.: Parallel programming with a pattern language. Int. J. Softw. Tools Technol. Transf. 3(2), 217\u2013234 (2001). \nhttps:\/\/doi.org\/10.1007\/s100090100045","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR31","volume-title":"Patterns for Parallel Programming","author":"TG Mattson","year":"2004","unstructured":"Mattson, T.G., Sanders, B., Massingill, B.: Patterns for Parallel Programming. Pearson Education, London (2004)"},{"key":"8_CR32","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 de Moura","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Norouzi, M., Wolf, F., Jannesari, A.: Automatic construct selection and variable classification in OpenMP. In: Proceedings of the International Conference on Supercomputing (ICS), Phoenix, AZ, USA, pp. 330\u2013341. ACM, Jun 2019. \nhttps:\/\/doi.org\/10.1145\/3330345.3330375","DOI":"10.1145\/3330345.3330375"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Steinh\u00f6fel, D.: Abstract Execution: automatically proving infinitely many programs. Ph.D. thesis, Technical University of Darmstadt, Department of Computer Science, Darmstadt, Germany (2020). \nhttps:\/\/doi.org\/10.25534\/tuprints-00008540","DOI":"10.25534\/tuprints-00008540"},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-030-03418-4_25","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Modeling","author":"D Steinh\u00f6fel","year":"2018","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Modular, correct compilation with automatic soundness proofs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 424\u2013447. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-03418-4_25"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Abstract Execution. In: Proceedings of the Third World Congress on Formal Methods - The Next 30 Years (FM), pp. 319\u2013336 (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-30942-8_20","DOI":"10.1007\/978-3-030-30942-8_20"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61470-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T18:07:06Z","timestamp":1603735626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61470-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030614690","9783030614706"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61470-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"27 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}