{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:35:07Z","timestamp":1761921307119,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031661488"},{"type":"electronic","value":"9783031661495"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-66149-5_8","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"146-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Solving Constrained Horn Clauses as\u00a0C Programs with\u00a0CHC2C"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6551-5860","authenticated-orcid":false,"given":"Levente","family":"Bajczi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8204-7595","authenticated-orcid":false,"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Bajczi, L., Moln\u00e1r, V.: Solving Constrained Horn Clauses as C Programs with CHC2C (2024). https:\/\/doi.org\/10.5281\/zenodo.10529452","key":"8_CR1","DOI":"10.5281\/zenodo.10529452"},{"doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 495\u2013522. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","key":"8_CR2","DOI":"10.1007\/978-3-031-30820-8_29"},{"doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verifiers and Validators of the 12th International Competition on Software Verification (SV-COMP 2023) (2023). https:\/\/doi.org\/10.5281\/ZENODO.7627829","key":"8_CR3","DOI":"10.5281\/ZENODO.7627829"},{"doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P., Lee, N.: Bridging hardware and software analysis with Btor2C: a word-level-circuit-to-C translator. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, ETAPS 2022. LNCS, vol. 13994, pp. 152\u2013172. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12","key":"8_CR4","DOI":"10.1007\/978-3-031-30820-8_12"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"publisher","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, 2\u20136 October 2017, p.\u00a09. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102233","key":"8_CR6","DOI":"10.23919\/FMCAD.2017.8102233"},{"doi-asserted-by":"publisher","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol.\u00a09780, pp. 510\u2013517. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29","key":"8_CR7","DOI":"10.1007\/978-3-319-41540-6_29"},{"unstructured":"Cok, D.R.: The SMT-LIBv2 Language and Tools: A Tutorial (2012). https:\/\/api.semanticscholar.org\/CorpusID:63272811","key":"8_CR8"},{"doi-asserted-by":"publisher","unstructured":"Daniel, J., Cimatti, A., Griggio, A., Tonetta, S., Mover, S.: Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol.\u00a09779, pp. 271\u2013291. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15","key":"8_CR9","DOI":"10.1007\/978-3-319-41528-4_15"},{"doi-asserted-by":"publisher","unstructured":"De Angelis, E., K., H.G.V.: CHC-COMP 2022: competition report. In: Hamilton, G.W., Kahsai, T., Proietti, M. (eds.) Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, HCVS\/VPT@ETAPS 2022, and 10th International Workshop on Verification and Program Transformation, Munich, 3rd April 2022. EPTCS, vol.\u00a0373, pp. 44\u201362 (2022). https:\/\/doi.org\/10.4204\/EPTCS.373.5","key":"8_CR10","DOI":"10.4204\/EPTCS.373.5"},{"doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: Ultimate TreeAutomizer (CHC-COMP Tool Description). In: Angelis, E.D., Fedyukovich, G., Tzevelekos, N., Ulbrich, M. (eds.) Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, HCVS\/PERR@ETAPS 2019, Prague, 6\u20137th April 2019. EPTCS, vol.\u00a0296, pp. 42\u201347 (2019).https:\/\/doi.org\/10.4204\/EPTCS.296.7","key":"8_CR11","DOI":"10.4204\/EPTCS.296.7"},{"doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Gurfinkel, A., Gupta, A.: Lazy but effective functional synthesis. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 92\u2013113. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_5","key":"8_CR12","DOI":"10.1007\/978-3-030-11245-5_5"},{"doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., R\u00fcmmer, P.: Competition report: CHC-COMP-21. In: Hojjat, H., Kafle, B. (eds.) Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021. EPTCS, vol.\u00a0344, pp. 91\u2013108 (2021). https:\/\/doi.org\/10.4204\/EPTCS.344.7","key":"8_CR13","DOI":"10.4204\/EPTCS.344.7"},{"doi-asserted-by":"publisher","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: Crnkovic, I., Chechik, M., Gr\u00fcnbacher, P. (eds.) ACM\/IEEE International Conference on Automated Software Engineering, ASE 2014, Vasteras, 15\u201319 September 2014, pp. 349\u2013360. ACM (2014). https:\/\/doi.org\/10.1145\/2642937.2642987","key":"8_CR14","DOI":"10.1145\/2642937.2642987"},{"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.) CAV 2015. LNCS, vol.\u00a09206, pp. 343\u2013361. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","key":"8_CR15","DOI":"10.1007\/978-3-319-21690-4_20"},{"doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, 30 October\u20132 November 2018, pp.\u00a01\u20137. IEEE (2018).https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","key":"8_CR16","DOI":"10.23919\/FMCAD.2018.8603013"},{"doi-asserted-by":"publisher","unstructured":"Hu, Q., Cyphert, J., D\u2019Antoni, L., Reps, T.W.: Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems, pp. 1128\u20131142. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385979","key":"8_CR17","DOI":"10.1145\/3385412.3385979"},{"unstructured":"Information Technology - Programming Languages - C. Standard, International Organization for Standardization (2011)","key":"8_CR18"},{"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.) CAV 2016. LNCS, vol.\u00a09779, pp. 352\u2013358. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","key":"8_CR19","DOI":"10.1007\/978-3-319-41528-4_19"},{"doi-asserted-by":"publisher","unstructured":"Kim, J., Hu, Q., D\u2019Antoni, L., Reps, T.W.: Semantics-guided synthesis. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434311","key":"8_CR20","DOI":"10.1145\/3434311"},{"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, 4\u20138 June 2011, pp. 222\u2013233. ACM (2011).https:\/\/doi.org\/10.1145\/1993498.1993525","key":"8_CR21","DOI":"10.1145\/1993498.1993525"},{"issue":"3","key":"8_CR22","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"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","key":"8_CR23","DOI":"10.1145\/3462205"},{"doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P.: Competition Report: CHC-COMP-20. In: Fribourg, L., Heizmann, M. (eds.) Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT\/HCVS@ETAPS 2020, Dublin, 25\u201326th April 2020. EPTCS, vol.\u00a0320, pp. 197\u2013219 (2020). https:\/\/doi.org\/10.4204\/EPTCS.320.15","key":"8_CR24","DOI":"10.4204\/EPTCS.320.15"},{"doi-asserted-by":"crossref","unstructured":"Somorjai, M., Dobos-Kov\u00e1cs, M., \u00c1d\u00e1m, Z., Bajczi, L., V\u00f6r\u00f6s, A.: Bottoms up for CHCs: novel transformation of linear constrained horn clauses to software verification. In: 10th Workshop on Horn Clauses for Verification and Synthesis (2023). https:\/\/ftsrg.mit.bme.hu\/paper-hcvs23-chc\/paper.pdf","key":"8_CR25","DOI":"10.4204\/EPTCS.402.11"},{"issue":"1","key":"8_CR26","doi-asserted-by":"publisher","first-page":"221","DOI":"10.3233\/SAT190123","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT Competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019). https:\/\/doi.org\/10.3233\/SAT190123","journal-title":"J. Satisf. Boolean Model. Comput."},{"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.) VMCAI 2022. LNCS, vol. 13182, pp. 425\u2013449. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21","key":"8_CR27","DOI":"10.1007\/978-3-030-94583-1_21"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:06:38Z","timestamp":1728716798000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}