{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T04:44:31Z","timestamp":1778215471229,"version":"3.51.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319572871","type":"print"},{"value":"9783319572888","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_17","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T06:45:05Z","timestamp":1491633905000},"page":"247-264","source":"Crossref","is-referenced-by-count":6,"title":["A Verification Technique for Deterministic Parallel Programs"],"prefix":"10.1007","author":[{"given":"Saeed","family":"Darabi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan C. C.","family":"Blom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"key":"17_CR1","unstructured":"Aviram, A., Ford, B.: Deterministic OpenMP for race-free parallelism. In: HotPar 2011, Berkeley, CA, USA, p. 4 (2011)"},{"key":"17_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: ACM SIGPLAN Notices, vol. 48, pp. 123\u2013134 (2013)","DOI":"10.1145\/2517327.2442529"},{"issue":"4","key":"17_CR3","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1016\/j.jpdc.2004.11.010","volume":"65","author":"MJ Berger","year":"2005","unstructured":"Berger, M.J., Aftosmis, M.J., Marshall, D.D., Murman, S.M.: Performance of a new CFD flow solver using a hybrid programming paradigm. J. Parallel Distrib. Comput. 65(4), 414\u2013423 (2005)","journal-title":"J. Parallel Distrib. Comput."},{"key":"17_CR4","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). doi: 10.1007\/978-3-319-06410-9_9"},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","volume":"95","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M., Mihel\u010di\u0107, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376\u2013388 (2014)","journal-title":"Sci. Comput. Program."},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-662-46675-9_14","volume-title":"Fundamental Approaches to Software Engineering","author":"S Blom","year":"2015","unstructured":"Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202\u2013217. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46675-9_14"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Botincan, M., Dodds, M., Jagannathan, S.: Resource-sensitive synchronization inference by abduction. In: POPL, pp. 309\u2013322 (2012)","DOI":"10.1145\/2103656.2103694"},{"key":"17_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2491522.2491525","volume":"35","author":"M Botin\u010dan","year":"2013","unstructured":"Botin\u010dan, M., Dodds, M., Jagannathan, S.: Proof-directed parallelization synthesis by separation logic. ACM Trans. Program. Lang. Syst. 35, 1\u201360 (2013)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR10","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. 2694, pp. 55\u201372. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44898-5_4"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Che, S., Boyer, M., Meng, J., Tarjan, D., Sheaffer, J.W., Lee, S.-H., Skadron, K.: Rodinia: a benchmark suite for heterogeneous computing. In: Workload Characterization, IISWC 2009, pp. 44\u201354 (2009)","DOI":"10.1109\/IISWC.2009.5306797"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Darabi, S., Blom, S.C.C., Huisman, M.: A verification technique for deterministic parallel programs (extended version). Technical report TR-CTIT-17-01, Centre for Telematics and Information Technology, University of Twente (2017)","DOI":"10.1007\/978-3-319-57288-8_17"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: ACM SIGPLAN Notices, pp. 259\u2013270 (2011)","DOI":"10.1145\/1926385.1926416"},{"issue":"10","key":"17_CR14","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-03237-0_6","volume-title":"Static Analysis","author":"C Hurlin","year":"2009","unstructured":"Hurlin, C.: Automatic parallelization and optimization of programs by proof rewriting. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 52\u201368. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03237-0_6"},{"key":"17_CR16","unstructured":"Jin, H.-Q., Frumkin, M., Yan, J.: The OpenMP implementation of NAS parallel Benchmarks and its performance (1999)"},{"issue":"1\u20133","key":"17_CR17","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR18","unstructured":"OpenMP Architecture Review Board: OpenMP API specification for parallel programming. http:\/\/openmp.org\/wp\/ . Accessed 28 Nov 2016"},{"key":"17_CR19","unstructured":"LLNL OpenMP Benchmarks. https:\/\/asc.llnl.gov\/CORAL-benchmarks\/ . Accessed 28 Nov 2016"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-642-38856-9_16","volume-title":"Static Analysis","author":"V Raychev","year":"2013","unstructured":"Raychev, V., Vechev, M., Yahav, E.: Automatic synthesis of deterministic concurrency. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 283\u2013303. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38856-9_16"},{"key":"17_CR21","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":"17_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\/1190216.1190234"},{"key":"17_CR23","unstructured":"VerCors project homepage, 28 September 2016. http:\/\/www.utwente.nl\/vercors\/"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T20:28:45Z","timestamp":1569011325000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}