{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:29Z","timestamp":1740098969806,"version":"3.37.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"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-69483-2_1","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T11:34:48Z","timestamp":1508153688000},"page":"3-22","source":"Crossref","is-referenced-by-count":3,"title":["General Lessons from a Rely\/Guarantee Development"],"prefix":"10.1007","author":[{"given":"Cliff B.","family":"Jones","sequence":"first","affiliation":[]},{"given":"Andrius","family":"Velykis","sequence":"additional","affiliation":[]},{"given":"Nisansala","family":"Yatapanage","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/579.587","volume":"6","author":"M Ben-Ari","year":"1984","unstructured":"Ben-Ari, M.: Algorithms for on-the-fly garbage collection. ACM Trans. Program. Lang. Syst. 6(3), 333\u2013344 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"1_CR2","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1007\/s00165-009-0141-8","volume":"22","author":"R Bornat","year":"2010","unstructured":"Bornat, R., Amjad, H.: Inter-process buffers in separation logic with rely-guarantee. Formal Aspects Comput. 22(6), 735\u2013772 (2010)","journal-title":"Formal Aspects Comput."},{"issue":"6","key":"1_CR3","doi-asserted-by":"crossref","first-page":"893","DOI":"10.1007\/s00165-011-0213-4","volume":"25","author":"R Bornat","year":"2013","unstructured":"Bornat, R., Amjad, H.: Explanation of two non-blocking shared-variable communication algorithms. Formal Aspects Comput. 25(6), 893\u2013931 (2013)","journal-title":"Formal Aspects Comput."},{"key":"1_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R-JR Back","year":"1998","unstructured":"Back, R.-J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Collette, P., Jones, C.B.: Enhancing the tractability of rely\/guarantee specifications in the development of interfering operations. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction, Chap. 10, pp. 277\u2013307. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0016"},{"issue":"4","key":"1_CR6","doi-asserted-by":"crossref","first-page":"807","DOI":"10.1093\/logcom\/exm030","volume":"17","author":"JW Coleman","year":"2007","unstructured":"Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely\/guarantee rules. J. Logic Comput. 17(4), 807\u2013841 (2007)","journal-title":"J. Logic Comput."},{"key":"1_CR7","unstructured":"Coleman, J.W.: Constructing a Tractable Reasoning Framework upon a Fine-Grained Structural Operational Semantics. Ph.D. thesis, Newcastle University, January 2008"},{"key":"1_CR8","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). doi: 10.1007\/978-3-642-00590-9_26"},{"key":"1_CR9","unstructured":"J\u00fcrgen Dingel. Systematic Parallel Programming. Ph.D. thesis, Carnegie Mellon University (2000). CMU-CS-99-172"},{"key":"1_CR10","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). doi: 10.1007\/978-3-642-14107-2_24"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173\u2013188. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71316-6_13"},{"issue":"3","key":"1_CR12","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1016\/j.scico.2006.10.001","volume":"64","author":"H Gao","year":"2007","unstructured":"Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free parallel and concurrent garbage collection by mark & sweep. Sci. Comput. Program. 64(3), 341\u2013374 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"1_CR13","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1093\/comjnl\/bxt005","volume":"56","author":"IJ Hayes","year":"2013","unstructured":"Hayes, I.J., Burns, A., Dongol, B., Jones, C.B.: Comparing degrees of non-determinism in expression evaluation. Comput. J. 56(6), 741\u2013755 (2013)","journal-title":"Comput. J."},{"key":"1_CR14","unstructured":"Hayes, I.J., Jones, C.B., Colvin, R.J.: Laws and semantics for rely-guarantee refinement. Technical Report CS-TR-1425, Newcastle University, July 2014"},{"issue":"2","key":"1_CR15","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/s10703-009-0083-z","volume":"36","author":"WH Hesselink","year":"2010","unstructured":"Hesselink, W.H., Lali, M.I.: Simple concurrent garbage collection almost without synchronization. Formal Methods Syst. Des. 36(2), 148\u2013166 (2010)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. In: Operating System Techniques, pp. 61\u201371. Academic Press (1972)","DOI":"10.1007\/978-1-4757-3472-0_6"},{"issue":"5, Part 2","key":"1_CR17","doi-asserted-by":"crossref","first-page":"972","DOI":"10.1016\/j.jlamp.2016.01.002","volume":"85","author":"CB Jones","year":"2016","unstructured":"Jones, C.B., Hayes, I.J.: Possible values: exploring a concept for concurrency. J. Logical Algebraic Methods Program. 85(5, Part 2), 972\u2013984 (2016). Articles dedicated to Prof. J. N. Oliveira on the occasion of his 60th birthday","journal-title":"J. Logical Algebraic Methods Program."},{"issue":"3","key":"1_CR18","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/s00165-014-0310-2","volume":"27","author":"CB Jones","year":"2015","unstructured":"Jones, C.B., Hayes, I.J., Colvin, R.J.: Balancing expressiveness in formal approaches to concurrency. Formal Aspects Comput. 27(3), 475\u2013497 (2015)","journal-title":"Formal Aspects Comput."},{"key":"1_CR19","unstructured":"Jones,C.B.: Development Methods for Computer Programs including a Notion of Interference. Ph.D. thesis, Oxford University, June 1981. Oxford University Computing Laboratory (now Computer Science) Technical Monograph PRG-25"},{"key":"1_CR20","volume-title":"Systematic Software Development using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall International, Englewood Cliffs (1990)","edition":"2"},{"issue":"2","key":"1_CR21","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00122417","volume":"8","author":"CB Jones","year":"1996","unstructured":"Jones, C.B.: Accommodating interference in the formal design of concurrent object-based programs. Formal Methods Syst. Des. 8(2), 105\u2013122 (1996)","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"1_CR22","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/s00165-010-0156-1","volume":"23","author":"CB Jones","year":"2011","unstructured":"Jones, C.B., Pierce, K.G.: Elucidating concurrent algorithms via layers of abstraction and reification. Formal Aspects Comput. 23(3), 289\u2013306 (2011)","journal-title":"Formal Aspects Comput."},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-22969-0_1","volume-title":"Software Engineering and Formal Methods","author":"CB Jones","year":"2015","unstructured":"Jones, C.B., Yatapanage, N.: Reasoning about separation using abstraction and reification. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 3\u201319. Springer, Cham (2015). doi: 10.1007\/978-3-319-22969-0_1"},{"key":"1_CR24","volume-title":"Programming from Specifications","author":"C Morgan","year":"1990","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall, New York (1990)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/3-540-44612-5_57","volume-title":"Mathematical Foundations of Computer Science 2000","author":"LP Nieto","year":"2000","unstructured":"Nieto, L.P., Esparza, J.: Verifying single and multi-mutator garbage collectors with owicki-gries in Isabelle\/HOL. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 619\u2013628. Springer, Heidelberg (2000). doi: 10.1007\/3-540-44612-5_57"},{"issue":"4","key":"1_CR26","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6(4), 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"issue":"1\u20133","key":"1_CR27","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":"1_CR28","unstructured":"Owicki, S.: Axiomatic Proof Techniques for Parallel Programs. Ph.D. thesis, Department of Computer Science, Cornell University (1975)"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-15057-9_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M Parkinson","year":"2010","unstructured":"Parkinson, M.: The next 700 separation logics. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 169\u2013182. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15057-9_12"},{"key":"1_CR30","unstructured":"Pierce, K.: Enhancing the Useability of Rely-Guaranteee Conditions for Atomicity Refinement. Ph.D. thesis, Newcastle University (2009)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-13321-3_20","volume-title":"Mathematics of Program Construction","author":"D Pavlovic","year":"2010","unstructured":"Pavlovic, D., Pepper, P., Smith, D.R.: Formal derivation of concurrent garbage collectors. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 353\u2013376. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-13321-3_20"},{"key":"1_CR32","unstructured":"Nieto, L.P.: Verification of parallel programs with the owicki-gries and rely-guarantee methods in Isabelle\/HOL. Ph.D. thesis, Institut f\u00fcr Informatic der Technischen Universitaet M\u00fcnchen (2001)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: TIME, pp. 99\u2013106 (2011)","DOI":"10.1109\/TIME.2011.12"},{"key":"1_CR34","unstructured":"St\u00f8len, K.: Development of Parallel Programs on Shared Data-Structures. Ph.D. thesis, Manchester University (1990). UMCS-91-1-1"},{"key":"1_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1377492.1377499","volume":"30","author":"N Torp-Smith","year":"2008","unstructured":"Torp-Smith, N., Birkedal, L., Reynolds, J.C.: Local reasoning about a copying garbage collector. ToPLaS 30, 1\u201358 (2008)","journal-title":"ToPLaS"},{"key":"1_CR36","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2007)"},{"issue":"4","key":"1_CR37","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0020-0190(87)90135-9","volume":"24","author":"LA Jan van de","year":"1987","unstructured":"van de Jan, L.A.: \u201cAlgorithms for on-the-fly garbage collection\u201d revisited. Inf. Process. Lett. 24(4), 211\u2013216 (1987)","journal-title":"Inf. Process. Lett."},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Bacon, D.F.: Correctness-preserving derivation of concurrent garbage collection algorithms. In: PLDI, pp. 341\u2013353 (2006)","DOI":"10.1145\/1133981.1134022"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/978-3-642-11957-6_32","volume-title":"Programming Languages and Systems","author":"J Wickerson","year":"2010","unstructured":"Wickerson, J., Dodds, M., Parkinson, M.: Explicit stabilisation for modular rely-guarantee reasoning. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 610\u2013629. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_32"},{"key":"1_CR40","unstructured":"Xu, Q.: A Theory of State-based Parallel Programming. Ph.D. thesis, Oxford University (1992)"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,27]],"date-time":"2024-06-27T20:11:29Z","timestamp":1719519089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}