{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:38Z","timestamp":1740122678709,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,8,16]],"date-time":"2021-08-16T00:00:00Z","timestamp":1629072000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,8,16]],"date-time":"2021-08-16T00:00:00Z","timestamp":1629072000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1007\/s10703-021-00378-0","type":"journal-article","created":{"date-parts":[[2021,8,16]],"date-time":"2021-08-16T18:02:57Z","timestamp":1629136977000},"page":"429-472","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic proofs of memory deallocation for a Whiley-to-C Compiler"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2334-1863","authenticated-orcid":false,"given":"Min-Hsien","family":"Weng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robi","family":"Malik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Utting","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,16]]},"reference":[{"key":"378_CR1","first-page":"529","volume-title":"Compilers: principles, techniques, and tools, chap 8","author":"AV Aho","year":"1986","unstructured":"Aho AV, Sethi R, Ullman JD (1986) Compilers: principles, techniques, and tools, chap 8. Addison-Wesley Longman Publishing Co. Inc, Boston, pp 529\u2013531"},{"key":"378_CR2","volume-title":"Why rust? Trustworthy, concurrent systems programming","author":"J Blandy","year":"2015","unstructured":"Blandy J (2015) Why rust? Trustworthy, concurrent systems programming. O\u2019Reilly, Sebastopol"},{"key":"378_CR3","doi-asserted-by":"publisher","unstructured":"Gopinath K, Hennessy JL (1989) Copy elimination in functional languages. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, NY, USA, POPL \u201989, pp 303\u2013314, https:\/\/doi.org\/10.1145\/75277.75304","DOI":"10.1145\/75277.75304"},{"key":"378_CR4","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-49727-7_20","volume-title":"Static analysis","author":"D Goyal","year":"1998","unstructured":"Goyal D, Paige R (1998) A new solution to the hidden copy problem. In: Levi G (ed) Static analysis. Springer, Berlin, pp 327\u2013348"},{"issue":"4","key":"378_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/989393.989401","volume":"39","author":"SL Graham","year":"2004","unstructured":"Graham SL, Kessler PB, McKusick MK (2004) Gprof: A call graph execution profiler. SIGPLAN Not 39(4):49\u201357. https:\/\/doi.org\/10.1145\/989393.989401","journal-title":"SIGPLAN Not"},{"key":"378_CR6","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-45213-3_4","volume-title":"Modular programming languages","author":"T Hoare","year":"2003","unstructured":"Hoare T (2003) The verifying compiler: a grand challenge for computing research. In: B\u00f6sz\u00f6rm\u00e9nyi L, Schojer P (eds) Modular programming languages. Springer, Berlin, pp 25\u201335"},{"key":"378_CR7","doi-asserted-by":"publisher","unstructured":"Hudak P, Bloss A (1985) The aggregate update problem in functional programming systems. In: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on principles of programming languages. ACM, New York, NY, USA, POPL \u201985, pp 300\u2013314, https:\/\/doi.org\/10.1145\/318593.318660","DOI":"10.1145\/318593.318660"},{"key":"378_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in computer science: modelling and reasoning about systems","author":"M Huth","year":"2004","unstructured":"Huth M, Ryan M (2004) Logic in computer science: modelling and reasoning about systems. Cambridge University Press, New York"},{"key":"378_CR9","unstructured":"ISO, IEC 9899:2011 (2011) Information technology-programming languages-C. Standard, International Organization for Standardization, Geneva, Switzerland"},{"key":"378_CR10","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-19861-8_3","volume-title":"Compiler construction","author":"N Lameed","year":"2011","unstructured":"Lameed N, Hendren L (2011) Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Knoop J (ed) Compiler construction. Springer, Berlin, pp 22\u201341"},{"key":"378_CR11","unstructured":"Leino R (2008) This is Boogie 2. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"378_CR12","doi-asserted-by":"crossref","unstructured":"Nethercote N, Seward J (2007) Valgrind: a framework for heavyweight dynamic binary instrumentation. In: ACM Sigplan notices. ACM, vol 42, pp 89\u2013100","DOI":"10.1145\/1273442.1250746"},{"key":"378_CR13","doi-asserted-by":"publisher","unstructured":"Odersky M (1991) How to make destructive updates less destructive. In: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, NY, USA, POPL \u201991, pp 25\u201336, https:\/\/doi.org\/10.1145\/99583.99590","DOI":"10.1145\/99583.99590"},{"key":"378_CR14","doi-asserted-by":"publisher","DOI":"10.1145\/3443420","author":"D Pearce","year":"2021","unstructured":"Pearce D (2021) A lightweight formalism for reference lifetimes and borrowing in Rust. ACM Trans Program Lang Syst. https:\/\/doi.org\/10.1145\/3443420","journal-title":"ACM Trans Program Lang Syst"},{"key":"378_CR15","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.scico.2015.09.006","volume":"113","author":"DJ Pearce","year":"2015","unstructured":"Pearce DJ, Groves L (2015) Designing a verifying compiler: lessons learned from developing Whiley. Sci Comput Program 113:191\u2013220. https:\/\/doi.org\/10.1016\/j.scico.2015.09.006","journal-title":"Sci Comput Program"},{"issue":"ICFP","key":"378_CR16","doi-asserted-by":"publisher","first-page":"17:1","DOI":"10.1145\/3110261","volume":"1","author":"J Protzenko","year":"2017","unstructured":"Protzenko J, Zinzindohou\u00e9 JK, Rastogi A, Ramananandro T, Wang P, Zanella-B\u00e9guelin S, Delignat-Lavaud A, Hri\u0163cu C, Bhargavan K, Fournet C, Swamy N (2017) Verified low-level programming embedded in F*. Proc ACM Program Lang 1(ICFP):17:1\u201317:29. https:\/\/doi.org\/10.1145\/3110261","journal-title":"Proc ACM Program Lang"},{"key":"378_CR17","doi-asserted-by":"publisher","unstructured":"Sastry AVS, Clinger W, Ariola Z (1993) Order-of-evaluation analysis for destructive updates in strict functional languages with flat aggregates. In: Proceedings of the conference on functional programming languages and computer architecture. ACM, New York, NY, USA, FPCA \u201993, pp 266\u2013275, https:\/\/doi.org\/10.1145\/165180.165222","DOI":"10.1145\/165180.165222"},{"key":"378_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17548-0","volume-title":"Compiler design: analysis and transformation","author":"H Seidl","year":"2012","unstructured":"Seidl H, Wilhelm R, Hack S (2012) Compiler design: analysis and transformation. Springer, Berlin"},{"issue":"11","key":"378_CR19","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/2426642.2259008","volume":"47","author":"R Shahriyar","year":"2012","unstructured":"Shahriyar R, Blackburn SM, Frampton D (2012) Down for the count? Getting reference counting back in the ring. ACM SIGPLAN Not 47(11):73\u201383. https:\/\/doi.org\/10.1145\/2426642.2259008","journal-title":"ACM SIGPLAN Not"},{"key":"378_CR20","doi-asserted-by":"publisher","unstructured":"Shahriyar R, Blackburn SM, Yang X, McKinley KS (2013) Taking off the gloves with reference counting immix. In: Conference on object-oriented programming systems, languages, and applications, OOPSLA, pp 93\u2013110, https:\/\/doi.org\/10.1145\/2509136.2509527","DOI":"10.1145\/2509136.2509527"},{"key":"378_CR21","doi-asserted-by":"crossref","unstructured":"Shankar N (2001) Static analysis for safe destructive updates in a functional language. In: Selected papers from the 11th international workshop on logic based program synthesis and transformation. Springer, London, UK, LOPSTR \u201901, pp 1\u201324","DOI":"10.1007\/3-540-45607-4_1"},{"issue":"1","key":"378_CR22","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/2914770.2837655","volume":"51","author":"N Swamy","year":"2016","unstructured":"Swamy N, Hri\u0163cu C, Keller C, Rastogi A, Delignat-Lavaud A, Forest S, Bhargavan K, Fournet C, Strub PY, Kohlweiss M, Zinzindohoue JK, Zanella-B\u00e9guelin S (2016) Dependent types and multi-monadic effects in F*. ACM SIGPLAN Not 51(1):256\u2013270. https:\/\/doi.org\/10.1145\/2914770.2837655","journal-title":"ACM SIGPLAN Not"},{"issue":"3","key":"378_CR23","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1017\/S0956796801003938","volume":"11","author":"M Wand","year":"2001","unstructured":"Wand M, Clinger WD (2001) Set constraints for destructive array update optimization. J Funct Program 11(3):319\u2013346. https:\/\/doi.org\/10.1017\/S0956796801003938","journal-title":"J Funct Program"},{"key":"378_CR24","unstructured":"Weng MH (2019) Efficient compilation of a verification-friendly programming language. PhD thesis, University of Waikato, Hamilton, New Zealand"},{"key":"378_CR25","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2016.01.005","volume":"320","author":"MH Weng","year":"2016","unstructured":"Weng MH, Utting M, Pfahringer B (2016) Bound analysis for Whiley programs. Electron Notes Theor Comput Sci 320:53\u201367. https:\/\/doi.org\/10.1016\/j.entcs.2016.01.005","journal-title":"Electron Notes Theor Comput Sci"},{"key":"378_CR26","doi-asserted-by":"crossref","unstructured":"Weng MH, Pfahringer B, Utting M (2017) Static techniques for reducing memory usage in the C implementation of Whiley programs. In: ACSW\u201917, ACM","DOI":"10.1145\/3014812.3014827"},{"issue":"3","key":"378_CR27","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1109\/TIT.1977.1055714","volume":"23","author":"J Ziv","year":"1977","unstructured":"Ziv J, Lempel A (1977) A universal algorithm for sequential data compression. IEEE Trans Inf Theory 23(3):337\u2013343. https:\/\/doi.org\/10.1109\/TIT.1977.1055714","journal-title":"IEEE Trans Inf Theory"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00378-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00378-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00378-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T12:11:28Z","timestamp":1638360688000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00378-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,16]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["378"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00378-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,8,16]]},"assertion":[{"value":"21 August 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 June 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}