{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:41:03Z","timestamp":1725928863774},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319723075"},{"type":"electronic","value":"9783319723082"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-72308-2_12","type":"book-chapter","created":{"date-parts":[[2017,12,14]],"date-time":"2017-12-14T18:25:15Z","timestamp":1513275915000},"page":"191-209","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["An Abstraction Technique for Describing Concurrent Program Behaviour"],"prefix":"10.1007","author":[{"given":"Wytse","family":"Oortwijn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Blom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marina","family":"Zaharieva-Stojanovski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,15]]},"reference":[{"issue":"1","key":"12_CR1","first-page":"1","volume":"11","author":"A Amighi","year":"2015","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1), 1\u201366 (2015)","journal-title":"LMCS"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"12_CR3","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). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_9"},{"key":"12_CR4","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). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_6"},{"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)","key":"12_CR5","DOI":"10.1145\/1040305.1040327"},{"key":"12_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. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P Rocha Pinto da","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"doi-asserted-by":"publisher","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: Steps in modular specifications for concurrent modules. In: MFPS, EPTCS, pp. 3\u201318 (2015). https:\/\/doi.org\/10.1016\/j.entcs.2015.12.002","key":"12_CR8","DOI":"10.1016\/j.entcs.2015.12.002"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-00590-9_26","volume-title":"Programming Languages and Systems","author":"M Dodds","year":"2009","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363\u2013377. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_26"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19\u201337. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76637-7_3"},{"key":"12_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-1-4471-2120-6_2","volume-title":"Algebra of Communicating Processes","author":"JF Groote","year":"1995","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of $$\\mu $$ \u03bc CRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes, pp. 26\u201362. Springer, London (1995). https:\/\/doi.org\/10.1007\/978-1-4471-2120-6_2"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-33518-1_37","volume-title":"Recent Advances in the Message Passing Interface","author":"K Honda","year":"2012","unstructured":"Honda, K., Marques, E.R.B., Martins, F., Ng, N., Vasconcelos, V.T., Yoshida, N.: Verification of MPI programs using session types. In: Tr\u00e4ff, J.L., Benkner, S., Dongarra, J.J. (eds.) EuroMPI 2012. LNCS, vol. 7490, pp. 291\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33518-1_37"},{"doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273\u2013284. ACM (2008)","key":"12_CR15","DOI":"10.1145\/1328438.1328472"},{"issue":"4","key":"12_CR16","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637\u2013650. ACM (2015)","key":"12_CR17","DOI":"10.1145\/2676726.2676980"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-662-54434-1_26","volume-title":"Programming Languages and Systems","author":"R Krebbers","year":"2017","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696\u2013723. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26"},{"issue":"1\u20133","key":"12_CR19","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."},{"unstructured":"Pang, J., van de Pol, J., Espada, M.: Abstraction of parallel uniform processes with data. In: SEFM, pp. 14\u201323. IEEE (2004)","key":"12_CR20"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-28756-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Popeea","year":"2012","unstructured":"Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 237\u2013251. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_17"},{"doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","key":"12_CR22","DOI":"10.1109\/LICS.2002.1029817"},{"doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77\u201387. ACM (2015)","key":"12_CR23","DOI":"10.1145\/2737924.2737964"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-662-46669-8_14","volume-title":"Programming Languages and Systems","author":"I Sergey","year":"2015","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Specifying and verifying concurrent algorithms with histories and subjectivity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 333\u2013358. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_14"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9"},{"doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377\u2013390 (2013)","key":"12_CR26","DOI":"10.1145\/2500365.2500600"},{"doi-asserted-by":"publisher","unstructured":"Zaharieva-Stojanovski, M.: Closer to reliable software: verifying functional behaviour of concurrent programs. Ph.D. thesis, University of Twente (2015). https:\/\/doi.org\/10.3990\/1.9789036539241","key":"12_CR27","DOI":"10.3990\/1.9789036539241"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72308-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T01:30:32Z","timestamp":1570498232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72308-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319723075","9783319723082"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72308-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}