{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T22:29:37Z","timestamp":1767997777967,"version":"3.49.0"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030449131","type":"print"},{"value":"9783030449148","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_18","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"484-514","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["RustHorn: CHC-Based Verification for Rust Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5208-3106","authenticated-orcid":false,"given":"Yusuke","family":"Matsushita","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, M\u00e9rida, Venezuela, March 11-15, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07180, pp. 46\u201361. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_7","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification (2018). https:\/\/doi.org\/10.3929\/ethz-b-000311092","DOI":"10.3929\/ethz-b-000311092"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Baranowski, M.S., He, S., Rakamaric, Z.: Verifying Rust programs with SMACK. In: Lahiri and Wang [42], pp. 528\u2013535. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_32","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: The Spec# experience. Commun. ACM 54(6), 81\u201391 (2011). https:\/\/doi.org\/10.1145\/1953122.1953145","DOI":"10.1145\/1953122.1953145"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, vol.\u00a09300, pp. 24\u201351. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 259\u2013270. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: Preventing data races and deadlocks. In: Ibrahim, M., Matsuoka, S. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle, Washington, USA, November 4-8, 2002. pp. 211\u2013230. ACM (2002). https:\/\/doi.org\/10.1145\/582419.582440","DOI":"10.1145\/582419.582440"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02694, pp. 55\u201372. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4","DOI":"10.1007\/3-540-44898-5_4"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a03855, pp. 427\u2013442. Springer (2006). https:\/\/doi.org\/10.1007\/11609773_28","DOI":"10.1007\/11609773_28"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10805, pp. 365\u2013384. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_20","DOI":"10.1007\/978-3-319-89960-2_20"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Champion, A., Kobayashi, N., Sato, R.: HoIce: An ICE-based non-linear Horn clause solver. In: Ryu, S. (ed.) Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11275, pp. 146\u2013156. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_8","DOI":"10.1007\/978-3-030-02768-1_8"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Clarke, D.G., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: Freeman-Benson, B.N., Chambers, C. (eds.) Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA \u201998), Vancouver, British Columbia, Canada, October 18-22, 1998. pp. 48\u201364. ACM (1998). https:\/\/doi.org\/10.1145\/286936.286947","DOI":"10.1145\/286936.286947"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05674, pp. 23\u201342. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"18_CR15","unstructured":"Coq Team: The Coq proof assistant (2020), https:\/\/coq.inria.fr\/"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. Journal of the ACM 23(4), 733\u2013742 (1976). https:\/\/doi.org\/10.1145\/321978.321991","DOI":"10.1145\/321978.321991"},{"key":"18_CR17","unstructured":"Erdin, M.: Verification of Rust Generics, Typestates, and Traits. Master\u2019s thesis, ETH Z\u00fcrich (2019)"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Kaufman, S.J., Bod\u00edk, R.: Sampling invariants from frequency distributions. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. pp. 100\u2013107. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102247","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 259\u2013277. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3), \u00a017 (2007). https:\/\/doi.org\/10.1145\/1232420.1232424","DOI":"10.1145\/1232420.1232424"},{"key":"18_CR21","unstructured":"Gondelman, L.: Un syst\u00e8me de types pragmatique pour la v\u00e9rification d\u00e9ductive des programmes. (A Pragmatic Type System for Deductive Verification). Ph.D. thesis, University of Paris-Saclay, France (2016), https:\/\/tel.archives-ouvertes.fr\/tel-01533090"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201912, Beijing, China - June 11 - 16, 2012. pp. 405\u2013416. ACM (2012). https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09206, pp. 343\u2013361. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Navas, J.A.: A context-sensitive memory model for verification of C\/C++ programs. In: Ranzato, F. (ed.) Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10422, pp. 148\u2013168. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_8","DOI":"10.1007\/978-3-319-66706-5_8"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016. pp. 338\u2013348. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950330","DOI":"10.1145\/2950290.2950330"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri and Wang [42], pp. 248\u2013266. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15","DOI":"10.1007\/978-3-030-01090-4_15"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Hahn, F.: Rust2Viper: Building a Static Verifier for Rust. Master\u2019s thesis, ETH Z\u00fcrich (2016). https:\/\/doi.org\/10.3929\/ethz-a-010669150","DOI":"10.3929\/ethz-a-010669150"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: A pearl in compositional verification. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 473\u2013485. ACM (2017). https:\/\/doi.org\/10.1145\/3009837","DOI":"10.1145\/3009837"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The Eldarica Horn solver. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp.\u00a01\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Horn, A.: On sentences which are true of direct unions of algebras. The Journal of Symbolic Logic 16(1), 14\u201321 (1951), http:\/\/www.jstor.org\/stable\/2268661","DOI":"10.2307\/2268661"},{"key":"18_CR31","unstructured":"Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: Ellis, C.S. (ed.) Proceedings of the General Track: 2002 USENIX Annual Technical Conference, June 10-15, 2002, Monterey, California, USA. pp. 275\u2013288. USENIX (2002), http:\/\/www.usenix.org\/publications\/library\/proceedings\/usenix02\/jim.html"},{"key":"18_CR32","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: RustBelt: Securing the foundations of the Rust programming language. PACMPL 2(POPL), 66:1\u201366:34 (2018). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"18_CR33","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, \u00a0e20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Jung, R., Lepigre, R., Parthasarathy, G., Rapoport, M., Timany, A., Dreyer, D., Jacobs, B.: The future is ours: Prophecy variables in separation logic. PACMPL 4(POPL), 45:1\u201345:32 (2020). https:\/\/doi.org\/10.1145\/3371113","DOI":"10.1145\/3371113"},{"key":"18_CR35","doi-asserted-by":"publisher","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: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. pp. 637\u2013650. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"18_CR36","unstructured":"Kahsai, T., Kersten, R., R\u00fcmmer, P., Sch\u00e4f, M.: Quantified heap invariants for object-oriented programs. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017. EPiC Series in Computing, vol.\u00a046, pp. 368\u2013384. EasyChair (2017)"},{"key":"18_CR37","doi-asserted-by":"publisher","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: A framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09779, pp. 352\u2013358. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: Analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, February 18-21, 2018. The Internet Society (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. pp. 222\u2013233. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993525","DOI":"10.1145\/1993498.1993525"},{"key":"18_CR40","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 17\u201334. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"18_CR41","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a02937, pp. 267\u2013281. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_22","DOI":"10.1007\/978-3-540-24622-0_22"},{"key":"18_CR42","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Wang, C. (eds.): Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11138. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4","DOI":"10.1007\/978-3-030-01090-4"},{"key":"18_CR43","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: Automatic pool allocation: Improving performance by controlling data structure layout in the heap. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005. pp. 129\u2013142. ACM (2005). https:\/\/doi.org\/10.1145\/1065010.1065027","DOI":"10.1145\/1065010.1065027"},{"key":"18_CR44","doi-asserted-by":"publisher","unstructured":"Lindner, M., Aparicius, J., Lindgren, P.: No panic! Verification of Rust programs by symbolic execution. In: 16th IEEE International Conference on Industrial Informatics, INDIN 2018, Porto, Portugal, July 18-20, 2018. pp. 108\u2013114. IEEE (2018). https:\/\/doi.org\/10.1109\/INDIN.2018.8471992","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"18_CR45","unstructured":"Matsakis, N.D.: Introducing MIR (2016), https:\/\/blog.rust-lang.org\/2016\/04\/19\/MIR.html"},{"key":"18_CR46","doi-asserted-by":"publisher","unstructured":"Matsakis, N.D., Klock II, F.S.: The Rust language. In: Feldman, M., Taft, S.T. (eds.) Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014. pp. 103\u2013104. ACM (2014). https:\/\/doi.org\/10.1145\/2663171.2663188","DOI":"10.1145\/2663171.2663188"},{"key":"18_CR47","doi-asserted-by":"crossref","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs (full version). CoRR (2020), https:\/\/arxiv.org\/abs\/2002.09002","DOI":"10.26226\/morressier.604907f41a80aac83ca25d55"},{"key":"18_CR48","unstructured":"Microsoft: Boogie: An intermediate verification language (2020), https:\/\/www.microsoft.com\/en-us\/research\/project\/boogie-an-intermediate-verification-language\/"},{"key":"18_CR49","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09195, pp. 378\u2013388. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"18_CR50","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Lecture Notes in Computer Science, vol.\u00a09583, pp. 41\u201362. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"18_CR51","unstructured":"Rust Community: The MIR (Mid-level IR) (2020), https:\/\/rust-lang.github.io\/rustc-guide\/mir\/index.html"},{"key":"18_CR52","unstructured":"Rust Community: Reference cycles can leak memory - the Rust programming language (2020), https:\/\/doc.rust-lang.org\/book\/ch15-06-reference-cycles.html"},{"key":"18_CR53","unstructured":"Rust Community: RFC 2025: Nested method calls (2020), https:\/\/rust-lang.github.io\/rfcs\/2025-nested-method-calls.html"},{"key":"18_CR54","unstructured":"Rust Community: RFC 2094: Non-lexical lifetimes (2020), https:\/\/rust-lang.github.io\/rfcs\/2094-nll.html"},{"key":"18_CR55","unstructured":"Rust Community: Rust programming language (2020), https:\/\/www.rust-lang.org\/"},{"key":"18_CR56","unstructured":"Rust Community: std::cell::RefCell - Rust (2020), https:\/\/doc.rust-lang.org\/std\/cell\/struct.RefCell.html"},{"key":"18_CR57","unstructured":"Rust Community: std::rc::Rc - Rust (2020), https:\/\/doc.rust-lang.org\/std\/rc\/struct.Rc.html"},{"key":"18_CR58","unstructured":"Rust Community: std::vec::Vec - Rust (2020), https:\/\/doc.rust-lang.org\/std\/vec\/struct.Vec.html"},{"key":"18_CR59","unstructured":"Rust Community: Two-phase borrows (2020), https:\/\/rust-lang.github.io\/rustc-guide\/borrow_check\/two_phase_borrows.html"},{"key":"18_CR60","doi-asserted-by":"publisher","unstructured":"Sato, R., Iwayama, N., Kobayashi, N.: Combining higher-order model checking with refinement type inference. In: Hermenegildo, M.V., Igarashi, A. (eds.) Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019. pp. 47\u201353. ACM (2019). https:\/\/doi.org\/10.1145\/3294032.3294081","DOI":"10.1145\/3294032.3294081"},{"key":"18_CR61","doi-asserted-by":"publisher","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Boehm, H., Jr., G.L.S. (eds.) Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. pp. 32\u201341. ACM Press (1996). https:\/\/doi.org\/10.1145\/237721.237727","DOI":"10.1145\/237721.237727"},{"key":"18_CR62","doi-asserted-by":"publisher","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. pp. 29\u201337. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932480","DOI":"10.1109\/LICS.2001.932480"},{"key":"18_CR63","doi-asserted-by":"publisher","unstructured":"Suenaga, K., Kobayashi, N.: Fractional ownerships for safe memory deallocation. In: Hu, Z. (ed.) Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05904, pp. 128\u2013143. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_11","DOI":"10.1007\/978-3-642-10672-9_11"},{"key":"18_CR64","doi-asserted-by":"publisher","unstructured":"Terauchi, T.: Checking race freedom via linear programming. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. pp. 1\u201310. ACM (2008). https:\/\/doi.org\/10.1145\/1375581.1375583","DOI":"10.1145\/1375581.1375583"},{"key":"18_CR65","doi-asserted-by":"publisher","unstructured":"Toman, J., Pernsteiner, S., Torlak, E.: crust: A bounded verifier for Rust. In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015. pp. 75\u201380. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/ASE.2015.77","DOI":"10.1109\/ASE.2015.77"},{"key":"18_CR66","unstructured":"Ullrich, S.: Electrolysis reference (2016), http:\/\/kha.github.io\/electrolysis\/"},{"key":"18_CR67","unstructured":"Ullrich, S.: Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis, Karlsruhe Institute of Technology (2016)"},{"key":"18_CR68","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, UK (2008), http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.612221"},{"key":"18_CR69","unstructured":"Z3 Team: The Z3 theorem prover (2020), https:\/\/github.com\/Z3Prover\/z3"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:11:27Z","timestamp":1656609087000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","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 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","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":"87","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":"27","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":"0","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":"31% - 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,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":"11-12","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}