{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T13:03:53Z","timestamp":1748351033520,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030480769"},{"type":"electronic","value":"9783030480776"}],"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-48077-6_2","type":"book-chapter","created":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T23:12:43Z","timestamp":1590102763000},"page":"6-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Adding Concurrency to a Sequential Refinement Tower"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Bodenm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,5,22]]},"reference":[{"key":"2_CR1","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret. Comput. Sci. 2, 253\u2013284 (1991). Also appeared as SRC Research Report 29"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-51285-3_42","volume-title":"PARLE \u201989 Parallel Architectures and Languages Europe","author":"RJR Back","year":"1989","unstructured":"Back, R.J.R.: A method for refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 199\u2013216. Springer, Heidelberg (1989). \nhttps:\/\/doi.org\/10.1007\/3-540-51285-3_42"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-642-18216-7","DOI":"10.1007\/978-3-642-18216-7"},{"key":"2_CR5","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). \nhttps:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"key":"2_CR6","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., et al.: 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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-10452-7_10","volume-title":"Formal Methods: Foundations and Applications","author":"K Damchoom","year":"2009","unstructured":"Damchoom, K., Butler, M.: Applying event and machine decomposition to a flash-based filestore in Event-B. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 134\u2013152. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-10452-7_10"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"de Roever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and in Object-Z: Foundations and Advanced Applications. FACIT. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/978-1-4471-5355-9\n\n. Second, revised edition 2014","DOI":"10.1007\/978-1-4471-5355-9"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Proceeding POPL 2009, pp. 2\u201315. ACM (2009)","DOI":"10.1145\/1594834.1480885"},{"issue":"6","key":"2_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and verifythis competition. Softw. Tools Techn. Transf. 17(6), 677\u2013694 (2015)","journal-title":"Softw. Tools Techn. Transf."},{"key":"2_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-319-29613-5_5","volume-title":"VSTTE 2015","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Inside a verified flash file system: transactions & garbage collection. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 73\u201393. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-29613-5_5"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Modular. Crash-Safe Refinement for ASMs with Submachines. Science of Computer Programming (SCP) (2016)","DOI":"10.1016\/j.scico.2016.04.009"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined resume. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187\u2013196. Springer, Heidelberg (1986). \nhttps:\/\/doi.org\/10.1007\/3-540-16442-1_14"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Software Engineering and Formal Methods (SEFM) 2005, pp. 137\u2013146. IEEE (2005)","DOI":"10.1109\/SEFM.2005.39"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume":"6617","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. NASA Formal Methods 6617, 41\u201355 (2011)","journal-title":"NASA Formal Methods"},{"key":"2_CR18","unstructured":"KIV proofs for wear leveling (2020). \nhttps:\/\/kiv.isse.de\/projects\/WearLeveling.html"},{"issue":"12","key":"2_CR19","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations - part i: untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995). Also: Technical Memo MIT\/LCS\/TM-486.b, Laboratory for Computer Science, MIT","DOI":"10.1006\/inco.1995.1134"},{"key":"2_CR21","unstructured":"Pf\u00e4hler, J.: A modular verification methodology for caching and lock-based concurrency in file systems. Ph.D. thesis, Universit\u00e4t Augsburg, Fakult\u00e4t f\u00fcr Informatik (2018). \nhttps:\/\/opus.bibliothek.uni-augsburg.de\/opus4\/frontdoor\/index\/index\/docId\/41890"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-66845-1_25","volume-title":"Integrated Formal Methods","author":"J Pf\u00e4hler","year":"2017","unstructured":"Pf\u00e4hler, J., Ernst, G., Bodenm\u00fcller, S., Schellhorn, G., Reif, W.: Modular verification of order-preserving write-back caches. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 375\u2013390. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66845-1_25"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-03077-7_15","volume-title":"Hardware and Software: Verification and Testing","author":"J Pf\u00e4hler","year":"2013","unstructured":"Pf\u00e4hler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Formal specification of an erase block management layer for flash memory. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 214\u2013229. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-03077-7_15"},{"key":"2_CR24","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic 15(4), 31:1\u201331:37 (2014)","DOI":"10.1145\/2629496"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Ernst, G., Pf\u00e4hler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014, vol. 8477. LNCS, pp. 9\u201324. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_2","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-33693-0_13","volume-title":"Integrated Formal Methods","author":"G Schellhorn","year":"2016","unstructured":"Schellhorn, G., Travkin, O., Wehrheim, H.: Towards a thread-local proof technique for starvation freedom. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 193\u2013209. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33693-0_13"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-23283-1_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2011","author":"B Tofan","year":"2011","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 239\u2013255. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-23283-1_16"},{"issue":"P3","key":"2_CR29","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/j.scico.2014.04.001","volume":"96","author":"B Tofan","year":"2014","unstructured":"Tofan, B., Travkin, O., Schellhorn, G., Wehrheim, H.: Two approaches for proving linearizability of multiset. Sci. Comput. Program. 96(P3), 297\u2013314 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149\u2013174 (1997)","journal-title":"Formal Aspects Comput."}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-48077-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T00:02:46Z","timestamp":1590105766000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-48077-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030480769","9783030480776"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-48077-6_2","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":"22 May 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ulm","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"27 May 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 May 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz2020.uni-ulm.de\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6 case study contributions, 6 PhD-Symposium-contributions, 2 invited papers. The conference was cancelled due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}