{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:30:11Z","timestamp":1769725811591,"version":"3.49.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Achieving high test coverage is important when developing blockchain smart contracts, but it could be challenging without automated reasoning tools. In this paper, we present <jats:sc>SolTG<\/jats:sc>, an automated test case generator for Solidity based on constrained Horn clauses (CHC). <jats:sc>SolTG<\/jats:sc> exhaustively enumerates symbolic path constraints from the contract\u2019s CHC representation and makes calls to the Satisfiability Modulo Theories (SMT) solver to find input values under which the contract exhibits the corresponding behavior. Test cases synthesized by <jats:sc>SolTG<\/jats:sc> have the form of a sequence of function calls over concrete values of input parameters which lead to a specific execution scenario. The tool supports multiple Solidity-specific features and is capable of exhibiting a high coverage for industrial-grade Solidity code. We present a detailed architecture of <jats:sc>SolTG<\/jats:sc> based on the existing translation of smart contracts into a CHC representation. We also present the experimental results for test generation on the regression and industrial benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_23","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"466-479","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["SolTG: A CHC-Based Solidity Test Case Generator"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-7843-7290","authenticated-orcid":false,"given":"Konstantin","family":"Britikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5329-993X","authenticated-orcid":false,"given":"Ilia","family":"Zlatkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5976-5153","authenticated-orcid":false,"given":"Leonardo","family":"Alt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8872-4913","authenticated-orcid":false,"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"23_CR1","unstructured":"Alshmrany, K.M., Menezes, R.S., Gadelha, M.R., Cordeiro, L.C.: FuSeBMC: a white-box fuzzer for finding security vulnerabilities in C programs. CoRR (2020). https:\/\/arxiv.org\/abs\/2012.11223"},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Solcmc: Solidity compiler\u2019s model checker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 325\u2013338. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"23_CR3","doi-asserted-by":"publisher","unstructured":"Bombarda, A., Gargantini, A., Calvagna, A.: Multi-thread combinatorial test generation with SMT solvers. In: Hong, J., Lanperne, M., Park, J.W., Cern\u00fd, T., Shahriar, H. (eds.) Proceedings of the 38th ACM\/SIGAPP Symposium on Applied Computing, SAC 2023, Tallinn, Estonia, March 27-31, 2023, pp. 1698\u20131705. ACM (2023). https:\/\/doi.org\/10.1145\/3555776.3577703","DOI":"10.1145\/3555776.3577703"},{"key":"23_CR4","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, December 8-10, 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008). http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Cadar, C., Nowack, M.: KLEE symbolic execution engine in 2019. Int. J. Softw. Tools Technol. Transf., 867\u2013870 (2021). https:\/\/doi.org\/10.1007\/S10009-020-00570-3","DOI":"10.1007\/S10009-020-00570-3"},{"key":"23_CR6","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Nov\u00e1k, J., Strejcek, J.: Symbiotic 8: parallel and targeted test generation - (competition contribution). In: Guerra, E., Stoelinga, M. (eds.) Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12649, pp. 368\u2013372. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_20","DOI":"10.1007\/978-3-030-71500-7_20"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Driessen, S.W., Nucci, D.D., Tamburri, D.A., van\u00a0den Heuvel, W.: Solar: automated test-suite generation for solidity smart contracts. Sci. Comput. Program. 232, 103036 (2024). https:\/\/doi.org\/10.1016\/J.SCICO.2023.103036","DOI":"10.1016\/J.SCICO.2023.103036"},{"key":"23_CR8","doi-asserted-by":"publisher","unstructured":"Ernst, G.: Korn - software verification with horn clauses (competition contribution). In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13994, pp. 559\u2013564. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_36","DOI":"10.1007\/978-3-031-30820-8_36"},{"key":"23_CR9","doi-asserted-by":"publisher","unstructured":"Esen, Z., R\u00fcmmer, P.: Tricera: Verifying C programs using the theory of heaps. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pp. 380\u2013391. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_45","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_45"},{"key":"23_CR10","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":"23_CR11","doi-asserted-by":"publisher","unstructured":"Jain, N., Kaneko, K., Sharma, S.: SKLEE: A dynamic symbolic analysis tool for ethereum smart contracts (tool paper). In: Schlingloff, B., Chai, M. (eds.) Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13550, pp. 244\u2013250. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_15","DOI":"10.1007\/978-3-031-17108-6_15"},{"key":"23_CR12","doi-asserted-by":"publisher","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.) Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III. Lecture Notes in Computer Science, vol. 12478, pp. 178\u2013194. Springer (2020).https:\/\/doi.org\/10.1007\/978-3-030-61467-6_12","DOI":"10.1007\/978-3-030-61467-6_12"},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. ACM Trans. Program. Lang. Syst. 43(4), 15:1\u201315:54 (2021). https:\/\/doi.org\/10.1145\/3462205","DOI":"10.1145\/3462205"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Olsthoorn, M., Stallenberg, D.M., van Deursen, A., Panichella, A.: SynTest-Solidity: automated test case generation and fuzzing for smart contracts. In: 44th IEEE\/ACM International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2022, Pittsburgh, PA, USA, May 22-24, 2022, pp. 202\u2013206. ACM\/IEEE (2022). https:\/\/doi.org\/10.1145\/3510454.3516869","DOI":"10.1145\/3510454.3516869"},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Pe\u00f1a, R., S\u00e1nchez-Hern\u00e1ndez, J., Garrido, M., Sagredo, J.: SMT-based test-case generation and validation for programs with complex specifications. In: L\u00f3pez-Garc\u00eda, P., Gallagher, J.P., Giacobazzi, R. (eds.) Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems - Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13160, pp. 188\u2013205. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-31476-6_10","DOI":"10.1007\/978-3-031-31476-6_10"},{"key":"23_CR17","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P.: Jayhorn: a java model checker. In: Murray, T., Ernst, G. (eds.) Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, FTfJP@ECOOP 2019, London, United Kingdom, July 15, 2019. p.\u00a01:1. ACM (2019). https:\/\/doi.org\/10.1145\/3340672.3341113","DOI":"10.1145\/3340672.3341113"},{"key":"23_CR18","doi-asserted-by":"publisher","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., W\u00fcstholz, V., Gurfinkel, A.: Verifying solidity smart contracts via communication abstraction in smartace. In: Finkbeiner, B., Wies, T. (eds.) Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13182, pp. 425\u2013449. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21","DOI":"10.1007\/978-3-030-94583-1_21"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-030-99527-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"I Zlatkin","year":"2022","unstructured":"Zlatkin, I., Fedyukovich, G.: Maximizing branch coverage with constrained horn clauses. In: TACAS 2022. LNCS, vol. 13244, pp. 254\u2013272. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_14"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:04:42Z","timestamp":1721934282000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}