{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:14:13Z","timestamp":1770293653295,"version":"3.49.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030888053","type":"print"},{"value":"9783030888060","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88806-0_21","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"429-452","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Compositional Verification of Smart Contracts Through Communication Abstraction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6708-2122","authenticated-orcid":false,"given":"Scott","family":"Wesley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria","family":"Christakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0516-1167","authenticated-orcid":false,"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5964-6792","authenticated-orcid":false,"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,13]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476\u2013495. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_28"},{"issue":"5","key":"21_CR2","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-015-0406-x","volume":"18","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 18(5), 495\u2013516 (2016). https:\/\/doi.org\/10.1007\/s10009-015-0406-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Allen, F.E.: Control flow analysis. In: Proceedings of a Symposium on Compiler Optimization, pp. 1\u201319. Association for Computing Machinery, New York, NY, USA (1970). https:\/\/doi.org\/10.1145\/800028.808479","DOI":"10.1145\/800028.808479"},{"issue":"2","key":"21_CR4","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/2951860.2951873","volume":"47","author":"R Bloem","year":"2016","unstructured":"Bloem, R., et al.: Decidability in parameterized verification. SIGACT News 47(2), 53\u201364 (2016). https:\/\/doi.org\/10.1145\/2951860.2951873","journal-title":"SIGACT News"},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Brent, L., Grech, N., Lagouvardos, S., Scholz, B., Smaragdakis, Y.: Ethainter: a smart contract security analyzer for composite vulnerabilities. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15\u201320 June 2020, pp. 454\u2013469. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385990","DOI":"10.1145\/3385412.3385990"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2005","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126\u2013141. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_9"},{"issue":"4","key":"21_CR7","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527\u2013550 (2003). https:\/\/doi.org\/10.1142\/S0129054103001881","journal-title":"Int. J. Found. Comput. Sci."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/11901433_6","volume-title":"Formal Methods and Software Engineering","author":"EA Emerson","year":"2006","unstructured":"Emerson, E.A., Trefler, R.J., Wahl, T.: Reducing model checking of the few to the one. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 94\u2013113. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_6"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-39799-8_8","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124\u2013140. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_8"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-24622-0_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with invisible ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 223\u2013238. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_19"},{"issue":"3","key":"21_CR11","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992). https:\/\/doi.org\/10.1145\/146637.146681","journal-title":"J. ACM"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Gershuni, E., et al.: Simple and precise static analysis of untrusted linux kernel extensions. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 1069\u20131084. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314590","DOI":"10.1145\/3314221.3314590"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Grech, N., Kong, M., Jurisevic, A., Brent, L., Scholz, B., Smaragdakis, Y.: Madmax: surviving out-of-gas conditions in ethereum smart contracts. In: Proceedings ACM Programming Language 2(OOPSLA), pp. 116:1\u2013116:27 (2018). https:\/\/doi.org\/10.1145\/3276486","DOI":"10.1145\/3276486"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. In: Proceedings ACM Programming Language 2(POPL), pp. 48:1\u201348:28 (2018). https:\/\/doi.org\/10.1145\/3158136","DOI":"10.1145\/3158136"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"21_CR16","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, 13\u201318 November 2016, pp. 338\u2013348. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950330","DOI":"10.1145\/2950290.2950330"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-41600-3_11","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"\u00c1 Hajdu","year":"2020","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 161\u2013179. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11"},{"key":"21_CR18","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Agnew, D., Claesen, L.J.M., Camposano, R. (eds.) Computer Hardware Description Languages and their Applications, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL 1993, sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26\u201328 April 1993. IFIP Transactions, vol. A-32, pp. 97\u2013111. North-Holland (1993)"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Jiang, B., Liu, Y., Chan, W.K.: Contractfuzzer: fuzzing smart contracts for vulnerability detection. In: Huchard, M., K\u00e4stner, C., Fraser, G. (eds.) Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3\u20137 September 2018, pp. 259\u2013269. ACM (2018). https:\/\/doi.org\/10.1145\/3238147.3238177","DOI":"10.1145\/3238147.3238177"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_55"},{"key":"21_CR21","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, 18\u201321 February 2018. The Internet Society (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-35873-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108\u2013127. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_9"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Fischer, P.C., Ullman, J.D. (eds.) Conference Record of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, pp. 194\u2013206. ACM Press, October 1973. https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"21_CR24","unstructured":"Kolb, J.: A Languge-Based Approach to Smart Contract Engineering. Ph.D. thesis, University of California at Berkeley, USA (2020)"},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Kolluri, A., Nikolic, I., Sergey, I., Hobor, A., Saxena, P.: Exploiting the laws of order in smart contracts. In: Zhang, D., M\u00f8ller, A. (eds.) Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, 15\u201319 July 2019, pp. 363\u2013373. ACM (2019). https:\/\/doi.org\/10.1145\/3293882.3330560","DOI":"10.1145\/3293882.3330560"},{"key":"21_CR26","unstructured":"Krupp, J., Rossow, C.: teether: Gnawing at ethereum to automatically exploit smart contracts. In: Enck, W., Felt, A.P. (eds.) 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, 15\u201317 August 2018, pp. 1317\u20131333. USENIX Association (2018)"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Weippl, E.R., Katzenbeisser, S., Kruegel, C., Myers, A.C., Halevi, S. (eds.) Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24\u201328 October 2016, pp. 254\u2013269. ACM (2016). https:\/\/doi.org\/10.1145\/2976749.2978309","DOI":"10.1145\/2976749.2978309"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-030-61467-6_12","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"M Marescotti","year":"2020","unstructured":"Marescotti, M., Otoni, R., Alt, L., Eugster, P., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Accurate smart contract verification through direct modelling. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 178\u2013194. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_12"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-030-32101-7_27","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2019","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: correct-by-design smart contracts for ethereum. In: Goldberg, I., Moore, T. (eds.) FC 2019. LNCS, vol. 11598, pp. 446\u2013465. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27"},{"key":"21_CR30","doi-asserted-by":"publisher","unstructured":"Mossberg, M., et al.: Manticore: a user-friendly symbolic execution framework for binaries and smart contracts. In: 34th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2019, San Diego, CA, USA, 11\u201315 November 2019, pp. 1186\u20131189. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00133","DOI":"10.1109\/ASE.2019.00133"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-49674-9_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2016","unstructured":"Namjoshi, K.S., Trefler, R.J.: Parameterized compositional model checking. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 589\u2013606. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_39"},{"key":"21_CR32","doi-asserted-by":"publisher","unstructured":"Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, 03\u201307 December 2018, pp. 653\u2013663. ACM (2018). https:\/\/doi.org\/10.1145\/3274694.3274743","DOI":"10.1145\/3274694.3274743"},{"key":"21_CR33","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 Informatica 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Informatica"},{"key":"21_CR34","doi-asserted-by":"publisher","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.T.: Verx: Safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18\u201321, 2020. pp. 1661\u20131677. IEEE (2020). DOI: https:\/\/doi.org\/10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"21_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_7"},{"key":"21_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-540-24732-6_20","volume-title":"Model Checking Software","author":"SF Siegel","year":"2004","unstructured":"Siegel, S.F., Avrunin, G.S.: Verification of MPI-Based software for scientific computation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 286\u2013303. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24732-6_20"},{"key":"21_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-18275-4_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"SF Siegel","year":"2011","unstructured":"Siegel, S.F., Gopalakrishnan, G.: Formal analysis of message passing. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 2\u201318. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_2"},{"key":"21_CR38","doi-asserted-by":"publisher","unstructured":"So, S., Lee, M., Park, J., Lee, H., Oh, H.: VERISMART: a highly precise safety verifier for ethereum smart contracts. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, 18\u201321 May 2020, pp. 1678\u20131694. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00032","DOI":"10.1109\/SP40000.2020.00032"},{"key":"21_CR39","doi-asserted-by":"publisher","unstructured":"Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.T.: Securify: Practical security analysis of smart contracts. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15\u201319 October 2018, pp. 67\u201382. ACM (2018). https:\/\/doi.org\/10.1145\/3243734.3243780","DOI":"10.1145\/3243734.3243780"},{"key":"21_CR40","doi-asserted-by":"publisher","unstructured":"Wang, S., Zhang, C., Su, Z.: Detecting nondeterministic payment bugs in ethereum smart contracts. In: Proceedings ACM Programming Language 3(OOPSLA), pp. 189:1\u2013189:29 (2019). https:\/\/doi.org\/10.1145\/3360615","DOI":"10.1145\/3360615"},{"key":"21_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-030-41600-3_7","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"Y Wang","year":"2020","unstructured":"Wang, Y., et al.: Formal verification of workflow policies for smart contracts in azure blockchain. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 87\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_7"},{"key":"21_CR42","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., W\u00fcstholz, V., Gurfinkel, A.: Compositional verification of smart contracts through communication abstraction (extended). CoRR abs\/2107.08583 (2021). https:\/\/arxiv.org\/abs\/2107.08583"},{"key":"21_CR43","doi-asserted-by":"publisher","unstructured":"W\u00fcstholz, V., Christakis, M.: Harvey: a greybox fuzzer for smart contracts. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, 8\u201313 November 2020, pp. 1398\u20131409. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3417064","DOI":"10.1145\/3368089.3417064"},{"key":"21_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-53288-8_7","volume-title":"Computer Aided Verification","author":"JE Zhong","year":"2020","unstructured":"Zhong, J.E., et al.: The move prover. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 137\u2013150. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_7"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88806-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:43:54Z","timestamp":1634147034000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88806-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888053","9783030888060"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88806-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chicago, IL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/staticanalysis.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"40","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":"18","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":"4","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":"45% - 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":"6","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)"}}]}}