{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:44:52Z","timestamp":1762508692428,"version":"3.40.3"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030945824"},{"type":"electronic","value":"9783030945831"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_21","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"425-449","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE"],"prefix":"10.1007","author":[{"given":"Scott","family":"Wesley","sequence":"first","affiliation":[]},{"given":"Maria","family":"Christakis","sequence":"additional","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[]},{"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"issue":"5","key":"21_CR1","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-015-0406-x","volume":"18","author":"P Abdulla","year":"2015","unstructured":"Abdulla, P., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 18(5), 495\u2013516 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0406-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Albert, E., Correas, J., Gordillo, P., Rom\u00e1n-D\u00edez, G., Rubio, A.: SAFEVM: a safety verifier for Ethereum 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. 386\u2013389. ACM (2019). https:\/\/doi.org\/10.1145\/3293882.3338999","DOI":"10.1145\/3293882.3338999"},{"issue":"6","key":"21_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986). https:\/\/doi.org\/10.1016\/0020-0190(86)90071-2","journal-title":"Inf. Process. Lett."},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Bacon, D.F., Sweeney, P.F.: Fast static analysis of C++ virtual function calls. In: Anderson, L., Coplien, J. (eds.) Proceedings of the 1996 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA 1996), San Jose, California, USA, 6\u201310 October 1996, pp. 324\u2013341. ACM (1996). https:\/\/doi.org\/10.1145\/236337.236371","DOI":"10.1145\/236337.236371"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44704-0_1","volume-title":"New Approaches in Software Measurement","author":"D Beyer","year":"2001","unstructured":"Beyer, D., Lewerentz, C., Simon, F.: Impact of inheritance on metrics for size, coupling, and cohesion in object-oriented systems. In: Dumke, R., Abran, A. (eds.) IWSM 2000. LNCS, vol. 2006, pp. 1\u201317. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44704-0_1"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Murray, T.C., Stefan, D. (eds.) Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, 24 October 2016, pp. 91\u201396. ACM (2016). https:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-662-46081-8_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263\u2013281. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_15"},{"issue":"2","key":"21_CR9","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_CR10","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_CR11","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, 8\u201310 December 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008)"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Juels, A., Wright, R.N., di Vimercati, S.D.C. (eds.) Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, Alexandria, VA, USA, 30 October\u20133 November 2006, pp. 322\u2013335. ACM (2006). https:\/\/doi.org\/10.1145\/1180405.1180445","DOI":"10.1145\/1180405.1180445"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: Dillon, L.K., Visser, W., Williams, L.A. (eds.) Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, 14\u201322 May 2016 - Companion Volume, pp. 589\u2013592. ACM (2016). https:\/\/doi.org\/10.1145\/2889160.2889163","DOI":"10.1145\/2889160.2889163"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Chen, H., Pendleton, M., Njilla, L., Xu, S.: A survey on Ethereum systems security: vulnerabilities, attacks, and defenses. ACM Comput. Surv. 53(3), 67:1\u201367:43 (2020). https:\/\/doi.org\/10.1145\/3391195","DOI":"10.1145\/3391195"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Durieux, T., Ferreira, J.F., Abreu, R., Cruz, P.: Empirical review of automated analysis tools on 47, 587 Ethereum smart contracts. In: Rothermel, G., Bae, D. (eds.) ICSE 2020: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June-19 July 2020, pp. 530\u2013541. ACM (2020). https:\/\/doi.org\/10.1145\/3377811.3380364","DOI":"10.1145\/3377811.3380364"},{"key":"21_CR17","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. Proc. ACM Program. Lang. 2(OOPSLA), 116:1\u2013116:27 (2018). https:\/\/doi.org\/10.1145\/3276486","DOI":"10.1145\/3276486"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Grieco, G., Song, W., Cygan, A., Feist, J., Groce, A.: Echidna: effective, usable, and fast fuzzing for smart contracts. In: Khurshid, S., Pasareanu, C.S. (eds.) ISSTA 2020: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, USA, 18\u201322 July 2020, pp. 557\u2013560. ACM (2020). https:\/\/doi.org\/10.1145\/3395363.3404366","DOI":"10.1145\/3395363.3404366"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2(POPL), 48:1\u201348:28 (2018). https:\/\/doi.org\/10.1145\/3158136","DOI":"10.1145\/3158136"},{"key":"21_CR21","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_CR22","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_CR23","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_CR24","doi-asserted-by":"publisher","unstructured":"He, J., Balunovic, M., Ambroladze, N., Tsankov, P., Vechev, M.T.: Learning to fuzz from symbolic execution with application to smart contracts. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, 11\u201315 November 2019, pp. 531\u2013548. ACM (2019). https:\/\/doi.org\/10.1145\/3319535.3363230","DOI":"10.1145\/3319535.3363230"},{"key":"21_CR25","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_CR26","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_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-030-30942-8_35","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"T Kasampalis","year":"2019","unstructured":"Kasampalis, T., et al.: IELE: a rigorously designed language and tool ecosystem for the blockchain. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 593\u2013610. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_35"},{"key":"21_CR28","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, October 1973, pp. 194\u2013206. ACM Press (1973). https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"21_CR29","unstructured":"Kolb, J.: A languge-based approach to smart contract engineering. Ph.D. thesis, University of California at Berkeley, USA (2020)"},{"key":"21_CR30","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_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"key":"21_CR32","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_CR33","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE\/ACM International Symposium on Code Generation and Optimization (CGO 2004), 20\u201324 March 2004, San Jose, CA, USA, pp. 75\u201388. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"21_CR34","unstructured":"LibFuzzer\u2013A library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"21_CR35","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_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-030-03427-6_33","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"M Marescotti","year":"2018","unstructured":"Marescotti, M., Blicha, M., Hyv\u00e4rinen, A.E.J., Asadi, S., Sharygina, N.: Computing exact worst-case gas consumption for smart contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 450\u2013465. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_33"},{"key":"21_CR37","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"},{"issue":"12","key":"21_CR38","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/96267.96279","volume":"33","author":"BP Miller","year":"1990","unstructured":"Miller, B.P., Fredriksen, L., So, B.: An empirical study of the reliability of UNIX utilities. Commun. ACM 33(12), 32\u201344 (1990). https:\/\/doi.org\/10.1145\/96267.96279","journal-title":"Commun. ACM"},{"key":"21_CR39","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_CR40","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_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-319-89963-3_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2018","unstructured":"Namjoshi, K.S., Trefler, R.J.: Symmetry reduction for the local mu-calculus. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 379\u2013395. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_22"},{"key":"21_CR42","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, 18\u201321 May 2020, pp. 1661\u20131677. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"21_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"key":"21_CR44","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_CR45","doi-asserted-by":"crossref","unstructured":"Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: SmartPulse: automated checking of temporal properties in smart contracts. In: 42nd IEEE Symposium on Security and Privacy. IEEE (2021)","DOI":"10.1109\/SP40001.2021.00085"},{"key":"21_CR46","unstructured":"Szabo, N.: Smart contracts: building blocks for digital markets (1996)"},{"key":"21_CR47","doi-asserted-by":"publisher","unstructured":"Torres, C.F., Sch\u00fctte, J., State, R.: Osiris: hunting for integer bugs in Ethereum smart contracts. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, 03\u201307 December 2018, pp. 664\u2013676. ACM (2018). https:\/\/doi.org\/10.1145\/3274694.3274737","DOI":"10.1145\/3274694.3274737"},{"key":"21_CR48","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_CR49","doi-asserted-by":"publisher","unstructured":"Wang, S., Zhang, C., Su, Z.: Detecting nondeterministic payment bugs in Ethereum smart contracts. Proc. ACM Program. Lang. 3(OOPSLA), 189:1\u2013189:29 (2019). https:\/\/doi.org\/10.1145\/3360615","DOI":"10.1145\/3360615"},{"key":"21_CR50","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_CR51","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-030-88806-0_21"},{"key":"21_CR52","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014)"},{"key":"21_CR53","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 2020: 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_CR54","unstructured":"Zalewski, M.: Technical whitepaper for AFL. http:\/\/lcamtuf.coredump.cx\/afl\/technical_details.txt"},{"key":"21_CR55","doi-asserted-by":"publisher","unstructured":"Zhang, W., Banescu, S., Pasos, L., Stewart, S.T., Ganesh, V.: MPro: combining static and symbolic analysis for scalable testing of smart contract. In: Wolter, K., Schieferdecker, I., Gallina, B., Cukier, M., Natella, R., Ivaki, N.R., Laranjeiro, N. (eds.) 30th IEEE International Symposium on Software Reliability Engineering, ISSRE 2019, Berlin, Germany, 28\u201331 October 2019, pp. 456\u2013462. IEEE (2019). https:\/\/doi.org\/10.1109\/ISSRE.2019.00052","DOI":"10.1109\/ISSRE.2019.00052"},{"key":"21_CR56","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Zhang, J., Zhang, D., Mu, Y.: Survey of directed fuzzy technology. In: 2018 IEEE 9th International Conference on Software Engineering and Service Science (ICSESS), pp. 696\u2013699. IEEE (2018). https:\/\/doi.org\/10.1109\/ICSESS.2018.8663772","DOI":"10.1109\/ICSESS.2018.8663772"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:06:10Z","timestamp":1642118770000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","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":"63","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":"23","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":"37% - 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)"}}]}}