{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:34:12Z","timestamp":1747888452491,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466742"},{"type":"electronic","value":"9783662466759"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46675-9_14","type":"book-chapter","created":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T20:24:38Z","timestamp":1427833478000},"page":"202-217","source":"Crossref","is-referenced-by-count":14,"title":["Verification of Loop Parallelisations"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Blom","sequence":"first","affiliation":[]},{"given":"Saeed","family":"Darabi","sequence":"additional","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Baghdadi, R., Cohen, A., Guelton, S., Verdoolaege, S., Inoue, J., Grosser, T., Kouveli, G., Kravets, A., Lokhmotov, A., Nugteren, C., Waters, F., Donaldson, A.F.: PENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs. CoRR, abs\/1302.5586 (2013)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to SIMD loop synthesis. In: PPoPP, pp. 123\u2013134 (2013)","DOI":"10.1145\/2517327.2442529"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M.: Verifying parallel loops with separation logic. In: PLACES, pp. 47\u201353 (2014)","DOI":"10.4204\/EPTCS.155.7"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M., Mihel\u010di\u0107, M.: Specification and verification of GPGPU programs. In: Science of Computer Programming (2014)","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 259\u2013270. ACM (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"issue":"1","key":"14_CR7","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/99.660313","volume":"5","author":"L. Dagum","year":"1998","unstructured":"Dagum, L., Menon, R.: OpenMP: an industry standard API for shared-memory programming. IEEE Computational Science & Engineering\u00a05(1), 46\u201355 (1998)","journal-title":"IEEE Computational Science & Engineering"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Gedell, T., H\u00e4hnle, R.: Automating verification of loops by parallelization. In: LPAR, pp. 332\u2013346 (2006)","DOI":"10.1007\/11916277_23"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-89330-1_13","volume-title":"Programming Languages and Systems","author":"C. Haack","year":"2008","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about java\u2019s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 171\u2013187. Springer, Heidelberg (2008)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-69149-5_41","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Hehner","year":"2008","unstructured":"Hehner, E.: Specified blocks. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 384\u2013391. Springer, Heidelberg (2008)"},{"issue":"10","key":"14_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"14_CR12","unstructured":"Juhasz, U., Kassios, I.T., M\u00fcller, P., Novacek, M., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. Technical report, ETH Zurich (2014)"},{"key":"14_CR13","unstructured":"Microsoft TPL, http:\/\/msdn.microsoft.com\/enus\/library\/dd460717.aspx"},{"issue":"6","key":"14_CR14","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1145\/2345156.2254124","volume":"47","author":"C.E. Oancea","year":"2012","unstructured":"Oancea, C.E., Rauchwerger, L.: Logical inference techniques for loop parallelization. SIGPLAN Not\u00a047(6), 509\u2013520 (2012)","journal-title":"SIGPLAN Not"},{"issue":"1\u20133","key":"14_CR15","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science\u00a0375(1\u20133), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Radoi, C., Dig, D.: Practical static race detection for java parallel loops. In: ISSTA, pp. 178\u2013190 (2013)","DOI":"10.1145\/2483760.2483765"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Rus, S., Pennings, M., Rauchwerger, L.: Sensitivity analysis for automatic parallelization on multi-cores. In: Proceedings of the 21st Annual International Conference on Supercomputing, ICS, pp. 263\u2013273. ACM (2007)","DOI":"10.1145\/1274971.1275008"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-11454-5_7","volume-title":"Using and Improving OpenMP for Devices, Tasks, and More","author":"J. Salamanca","year":"2014","unstructured":"Salamanca, J., Mattos, L., Araujo, G.: Loop-carried dependence verification in openMP. In: DeRose, L., de Supinski, B.R., Olivier, S.L., Chapman, B.M., M\u00fcller, M.S. (eds.) IWOMP 2014. LNCS, vol.\u00a08766, pp. 87\u2013102. Springer, Heidelberg (2014)"},{"key":"14_CR20","unstructured":"State of the Lambda: Libraries Edition, http:\/\/cr.openjdk.java.net\/~briangoetz\/lambda\/lambda-libraries-final.html"},{"key":"14_CR21","unstructured":"Threading Building Blocks, http:\/\/threadingbuildingblocks.org"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 97\u2013108. ACM (2007)","DOI":"10.1145\/1190215.1190234"},{"key":"14_CR23","unstructured":"Viper project website, http:\/\/www.pm.inf.ethz.ch\/research\/viper"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46675-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:47:53Z","timestamp":1747856873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46675-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466742","9783662466759"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46675-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}