{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:40:08Z","timestamp":1748806808625,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_16","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"226-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Effectively Eliminating Auxiliaries"],"prefix":"10.1007","author":[{"given":"Stijn","family":"de Gouw","sequence":"first","affiliation":[]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/BF00289262","volume":"15","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Recursive assertions and parallel programs. Acta Inf. 15, 219\u2013232 (1981)","journal-title":"Acta Inf."},{"issue":"4","key":"16_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90058-6","volume":"8","author":"KR Apt","year":"1979","unstructured":"Apt, K.R., Bergstra, J.A., Meertens, L.G.L.T.: Recursive assertions are not enough - or are they? Theor. Comput. Sci. 8, 73\u201387 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR4","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, London (2009)"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212\u2013232 (2005)","journal-title":"STTT"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/BF00263992","volume":"13","author":"EM Clarke","year":"1980","unstructured":"Clarke, E.M.: Proving correctness of coroutines without history variables. Acta Inf. 13, 169\u2013188 (1980)","journal-title":"Acta Inf."},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/BF00571463","volume":"2","author":"M Clint","year":"1973","unstructured":"Clint, M.: Program proving: coroutines. Acta Inf. 2, 50\u201363 (1973)","journal-title":"Acta Inf."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-35843-2_19","volume-title":"SOFSEM 2013: Theory and Practice of Computer Science","author":"S de Gouw","year":"2013","unstructured":"de Gouw, S., de Boer, F., Ahrendt, W., Bubel, R.: Weak arithmetic completeness of object-oriented first-order assertion networks. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 207\u2013219. Springer, Heidelberg (2013)"},{"issue":"2","key":"16_CR9","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10817-013-9300-y","volume":"53","author":"S de Gouw","year":"2014","unstructured":"de Gouw, S., de Boer, F.S., Rot, J.: Proof pearl: the KeY to correct and stable sorting. J. Autom. Reasoning 53(2), 129\u2013139 (2014)","journal-title":"J. Autom. Reasoning"},{"issue":"10","key":"16_CR10","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"16_CR11","first-page":"61","volume-title":"Operating System Techniques","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. In: Hoare, C.A.R., Perrott, R.H. (eds.) Operating System Techniques, pp. 61\u201371. Academic Press, New York (1972)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78663-4_1","volume-title":"Trustworthy Global Computing","author":"M Hofmann","year":"2008","unstructured":"Hofmann, M., Pavlova, M.: Elimination of ghost variables in program logics. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 1\u201320. Springer, Heidelberg (2008)"},{"issue":"5","key":"16_CR13","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/360051.360079","volume":"19","author":"JH Howard","year":"1976","unstructured":"Howard, J.H.: Proving monitors. Commun. ACM 19(5), 273\u2013279 (1976)","journal-title":"Commun. ACM"},{"key":"16_CR14","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Technical report ECS-LFCS-98-399, Laboratory for Foundations of Computer Science, University of Edinburgh (1998)"},{"issue":"5","key":"16_CR15","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11(5), 541\u2013566 (1999)","journal-title":"Formal Aspects Comput."},{"issue":"2","key":"16_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002. LNCS, vol. 2471, pp. 103\u2013119. Springer, Heidelberg (2002)"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(83)90009-9","volume":"24","author":"E-R Olderog","year":"1983","unstructured":"Olderog, E.-R.: On the notion of expressiveness and the rule of adaption. Theor. Comput. Sci. 24, 337\u2013347 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR19","series-title":"Outstanding Dissertations in the Computer Sciences","volume-title":"Axiomatic Proof Techniques for Parallel Programs","author":"SS Owicki","year":"1975","unstructured":"Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York (1975)"},{"key":"16_CR20","doi-asserted-by":"publisher","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 Inf. 6, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Proceedings, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:20:54Z","timestamp":1748805654000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}