{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T19:34:00Z","timestamp":1772134440712,"version":"3.50.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319668444","type":"print"},{"value":"9783319668451","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-66845-1_7","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"102-110","source":"Crossref","is-referenced-by-count":73,"title":["The VerCors Tool Set: Verification of Parallel and Concurrent Software"],"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":[]},{"given":"Wytse","family":"Oortwijn","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-22969-0_5","volume-title":"Software Engineering and Formal Methods","author":"A Amighi","year":"2015","unstructured":"Amighi, A., Darabi, S., Blom, S., Huisman, M.: Specification and verification of atomic operations in GPGPU programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 69\u201383. Springer, Cham (2015). doi: 10.1007\/978-3-319-22969-0_5"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA, pp. 113\u2013132. ACM (2012)","DOI":"10.1145\/2384616.2384625"},{"key":"7_CR4","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":"7_CR5","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":"7_CR6","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":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-22969-0_6","volume-title":"Software Engineering and Formal Methods","author":"S Blom","year":"2015","unstructured":"Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84\u201398. Springer, Cham (2015). doi: 10.1007\/978-3-319-22969-0_6"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_2"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-57288-8_17","volume-title":"NASA Formal Methods","author":"S Darabi","year":"2017","unstructured":"Darabi, S., Blom, S.C.C., Huisman, M.: A verification technique for deterministic parallel programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 247\u2013264. Springer, Cham (2017). doi: 10.1007\/978-3-319-57288-8_17"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Huisman, M., Klebanov, V., Monahan, R., Tautschnig, M.: VerifyThis 2015: a program verification competition. Int. J. Softw. Tools Technol. Transfer (2016)","DOI":"10.1007\/s10009-016-0438-x"},{"key":"7_CR12","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). doi: 10.1007\/978-3-642-20398-5_4"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195\u2013222. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03829-7_7"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49122-5_2"},{"issue":"1\u20133","key":"7_CR15","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":"7_CR16","doi-asserted-by":"crossref","unstructured":"Oortwijn, W., Blom, S., Gurov, D., Huisman, M., Zaharieva-Stojanovski, M.: An abstraction technique for describing concurrent program behaviour. In: VSTTE (2017, to appear)","DOI":"10.1007\/978-3-319-72308-2_12"},{"key":"7_CR17","unstructured":"OpenMP Architecture Review Board, OpenMP API Specification for Parallel Programming. http:\/\/openmp.org\/wp\/ . Accessed 18 Oct 2016"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_40"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Concurrent separation logic and operational semantics. In: MFPS. ENTCS, vol. 276, pp. 335\u2013351 (2011)","DOI":"10.1016\/j.entcs.2011.09.029"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T16:51:43Z","timestamp":1570035103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}