{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T19:43:56Z","timestamp":1782848636532,"version":"3.54.5"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T00:00:00Z","timestamp":1782777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101076510"],"award-info":[{"award-number":["101076510"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>A Constrained Horn Clause (CHC) is a specific type of logic formula  \nthat contains uninterpreted predicates. CHC formulas are often used by  \nstatic program analyzers to encode program properties, which are then  \nverified using CHC solvers. The solvers themselves are complex tools  \nand may contain bugs, which can lead to verifying unsafe programs,  \nflagging safe programs as unsafe, or providing analyzers with  \nincorrect invariants and counterexamples. It is, therefore, crucial to  \ndevelop techniques for systematically testing CHC solvers.<\/jats:p>\n                  <jats:p>In this paper, we present the first interrogation-testing technique  \nfor CHC solvers, which we implement in a tool called HornGator. Our  \ntechnique uses witnesses generated by the solver under test to form  \nnew CHC instances. It also integrates a knowledge base maintaining a  \nhistory of past solver queries. All this information helps HornGator  \ngenerate more diverse instances, thereby improving its bug-finding  \neffectiveness. As a result, HornGator found 21 unique bugs in five  \nstate-of-the-art CHC solvers, all of which are confirmed by the  \ndevelopers, 18 are fixed, and eight are of the highest severity.<\/jats:p>","DOI":"10.1145\/3797104","type":"journal-article","created":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T17:06:14Z","timestamp":1782839174000},"page":"1692-1711","source":"Crossref","is-referenced-by-count":0,"title":["Interrogation Testing of CHC Solvers"],"prefix":"10.1145","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4137-5163","authenticated-orcid":false,"given":"David","family":"Kaindlstorfer","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6375-0421","authenticated-orcid":false,"given":"Anastasia","family":"Isychev","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1496-1104","authenticated-orcid":false,"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[{"name":"Diligence Security, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2649-1958","authenticated-orcid":false,"given":"Maria","family":"Christakis","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,30]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"CHC-COMP. https:\/\/chc-comp.github.io."},{"key":"e_1_2_1_2_1","unstructured":"n. d.]. The Satisfiability Modulo Theories Library. http:\/\/smtlib.cs.uiowa.edu."},{"key":"e_1_2_1_3_1","first-page":"24","article-title":"Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II (LNCS, Vol. 9300)","author":"Bj\u00f8rner Nikolaj S.","year":"2015","unstructured":"Nikolaj S. Bj\u00f8rner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II (LNCS, Vol. 9300). Springer, 24-51.","journal-title":"Springer"},{"key":"e_1_2_1_4_1","first-page":"209","article-title":"The Golem Horn Solver. In CAV (LNCS, Vol. 13965)","author":"Blicha Martin","year":"2023","unstructured":"Martin Blicha, Konstantin Britikov, and Natasha Sharygina. 2023. The Golem Horn Solver. In CAV (LNCS, Vol. 13965). Springer, 209-223.","journal-title":"Springer"},{"key":"e_1_2_1_5_1","first-page":"45","article-title":"StringFuzz: A Fuzzer for String Solvers. In CAV (LNCS, Vol. 10982)","author":"Blotsky Dmitry","year":"2018","unstructured":"Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers. In CAV (LNCS, Vol. 10982). Springer, 45-51.","journal-title":"Springer"},{"key":"e_1_2_1_6_1","first-page":"1","article-title":"Finding and Understanding Incompleteness Bugs in SMT Solvers","volume":"43","author":"Bringolf Mauro","year":"2022","unstructured":"Mauro Bringolf, Dominik Winterer, and Zhendong Su. 2022. Finding and Understanding Incompleteness Bugs in SMT Solvers. In ASE. ACM, 43:1-43:10.","journal-title":"ASE. ACM"},{"key":"e_1_2_1_7_1","first-page":"1","article-title":"Fuzzing and Delta-Debugging SMT Solvers","author":"Brummayer Robert","year":"2009","unstructured":"Robert Brummayer and Armin Biere. 2009. Fuzzing and Delta-Debugging SMT Solvers. In SMT. ACM, 1-5.","journal-title":"SMT. ACM"},{"key":"e_1_2_1_8_1","first-page":"44","article-title":"Automated Testing and Debugging of SAT and QBF Solvers. In SAT (LNCS, Vol. 6175)","author":"Brummayer Robert","year":"2010","unstructured":"Robert Brummayer, Florian Lonsing, and Armin Biere. 2010. Automated Testing and Debugging of SAT and QBF Solvers. In SAT (LNCS, Vol. 6175). Springer, 44-57.","journal-title":"Springer"},{"key":"e_1_2_1_9_1","first-page":"1459","article-title":"Automatically Testing String Solvers","author":"Bugariu Alexandra","year":"2020","unstructured":"Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically Testing String Solvers. In ICSE. ACM, 1459-1470.","journal-title":"ICSE. ACM"},{"key":"e_1_2_1_10_1","first-page":"768","article-title":"Automatically Testing Implementations of Numerical Abstract Domains","author":"Bugariu Alexandra","year":"2018","unstructured":"Alexandra Bugariu, Valentin W\u00fcstholz, Maria Christakis, and Peter M\u00fcller. 2018. Automatically Testing Implementations of Numerical Abstract Domains. In ASE. ACM, 768-778.","journal-title":"ASE. ACM"},{"key":"e_1_2_1_11_1","first-page":"1","article-title":"A Survey of Compiler","volume":"53","author":"Chen Junjie","year":"2020","unstructured":"Junjie Chen, Jibesh Patra, Michael Pradel, Yingfei Xiong, Hongyu Zhang, Dan Hao, and Lu Zhang. 2020. A Survey of Compiler Testing. Comput. Surv. 53 (2020), 4:1-4:36. Issue 1.","journal-title":"Testing. Comput. Surv."},{"key":"e_1_2_1_12_1","volume-title":"Metamorphic Testing: A New Approach for Generating Next Test Cases. Technical Report HKUST-CS98-01. HKUST.","author":"Chen Tsong Yueh","year":"1998","unstructured":"Tsong Yueh Chen, S. C. Cheung, and Siu-Ming Yiu. 1998. Metamorphic Testing: A New Approach for Generating Next Test Cases. Technical Report HKUST-CS98-01. HKUST."},{"key":"e_1_2_1_13_1","volume-title":"HCVS\/PERR@ETAPS (EPTCS","author":"Dietsch Daniel","unstructured":"Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. 2019. Ultimate TreeAutomizer (CHC-COMP Tool Description). In HCVS\/PERR@ETAPS (EPTCS, Vol. 296). 42-47."},{"key":"e_1_2_1_14_1","volume-title":"Bj\u00f8rner","author":"Gurfinkel Arie","year":"2019","unstructured":"Arie Gurfinkel and Nikolaj S. Bj\u00f8rner. 2019. The Science, Art, and Magic of Constrained Horn Clauses. In SYNASC. IEEE Computer Society, 6-10."},{"key":"e_1_2_1_15_1","first-page":"343","article-title":"The SeaHorn Verification Framework. In CAV (LNCS, Vol. 9206)","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV (LNCS, Vol. 9206). Springer, 343-361.","journal-title":"Springer"},{"key":"e_1_2_1_16_1","first-page":"1","article-title":"The ELDARICA Horn Solver","author":"Hojjat Hossein","year":"2018","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The ELDARICA Horn Solver. In FMCAD. IEEE Computer Society, 1-7.","journal-title":"FMCAD. IEEE Computer Society"},{"key":"e_1_2_1_17_1","first-page":"352","article-title":"JayHorn: A Framework for Verifying Java Programs. In CAV (LNCS, Vol. 9779)","author":"Kahsai Temesghen","year":"2016","unstructured":"Temesghen Kahsai, Philipp R\u00fcmmer, Huascar Sanchez, and Martin Sch\u00e4f. 2016. JayHorn: A Framework for Verifying Java Programs. In CAV (LNCS, Vol. 9779). Springer, 352-358.","journal-title":"Springer"},{"key":"e_1_2_1_18_1","first-page":"319","article-title":"Interrogation Testing of Program Analyzers for Soundness and Precision Issues","author":"Kaindlstorfer David","year":"2024","unstructured":"David Kaindlstorfer, Anastasia Isychev, Valentin W\u00fcstholz, and Maria Christakis. 2024. Interrogation Testing of Program Analyzers for Soundness and Precision Issues. In ASE. ACM, 319-330.","journal-title":"ASE. ACM"},{"key":"e_1_2_1_19_1","first-page":"590","article-title":"Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing","author":"Kapus Timotej","year":"2017","unstructured":"Timotej Kapus and Cristian Cadar. 2017. Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing. In ASE. IEEE Computer Society, 590-600.","journal-title":"ASE. IEEE Computer Society"},{"key":"e_1_2_1_20_1","first-page":"2224","article-title":"Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations","author":"Kim Jongwook","year":"2023","unstructured":"Jongwook Kim, Sunbeom So, and Hakjoo Oh. 2023. Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations. In ICSE. IEEE Computer Society, 2224-2236.","journal-title":"ICSE. IEEE Computer Society"},{"key":"e_1_2_1_21_1","first-page":"239","article-title":"Differentially Testing Soundness and Precision of Program Analyzers","author":"Klinger Christian","year":"2019","unstructured":"Christian Klinger, Maria Christakis, and Valentin W\u00fcstholz. 2019. Differentially Testing Soundness and Precision of Program Analyzers. In ISSTA. ACM, 239-250.","journal-title":"ISSTA. ACM"},{"key":"e_1_2_1_22_1","first-page":"17","article-title":"SMT-Based Model Checking for Recursive Programs. In CAV (LNCS, Vol. 8559)","author":"Komuravelli Anvesh","year":"2014","unstructured":"Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In CAV (LNCS, Vol. 8559). Springer, 17-34.","journal-title":"Springer"},{"key":"e_1_2_1_23_1","first-page":"639","article-title":"Metamorphic Testing of Datalog Engines","author":"Mansur Muhammad Numair","year":"2021","unstructured":"Muhammad Numair Mansur, Maria Christakis, and Valentin W\u00fcstholz. 2021. Metamorphic Testing of Datalog Engines. In ESEC\/FSE. ACM, 639-650.","journal-title":"ESEC\/FSE. ACM"},{"key":"e_1_2_1_24_1","first-page":"701","article-title":"Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing","author":"Mansur Muhammad Numair","year":"2020","unstructured":"Muhammad Numair Mansur, Maria Christakis, Valentin W\u00fcstholz, and Fuyuan Zhang. 2020. Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing. In ESEC\/FSE. ACM, 701-712.","journal-title":"ESEC\/FSE. ACM"},{"key":"e_1_2_1_25_1","first-page":"236","article-title":"Dependency-Aware Metamorphic Testing of Datalog Engines","author":"Mansur Muhammad Numair","year":"2023","unstructured":"Muhammad Numair Mansur, Valentin W\u00fcstholz, and Maria Christakis. 2023. Dependency-Aware Metamorphic Testing of Datalog Engines. In ISSTA. ACM, 236-247.","journal-title":"ISSTA. ACM"},{"key":"e_1_2_1_26_1","first-page":"484","article-title":"RustHorn: CHC-Based Verification for Rust Programs. In ESOP (LNCS, Vol. 12075)","author":"Matsushita Yusuke","year":"2020","unstructured":"Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. 2020. RustHorn: CHC-Based Verification for Rust Programs. In ESOP (LNCS, Vol. 12075). Springer, 484-514.","journal-title":"Springer"},{"key":"e_1_2_1_27_1","first-page":"100","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman. 1998. Differential Testing for Software. Digital Technical Journal 10 (1998), 100-107. Issue 1.","journal-title":"Digital Technical Journal"},{"key":"e_1_2_1_28_1","volume-title":"Verif. Reliab. 27","author":"Midtgaard Jan","year":"2017","unstructured":"Jan Midtgaard and Anders M\u00f8ller. 2017. QuickChecking Static Analysis Properties. Softw. Test., Verif. Reliab. 27 (2017). Issue 6."},{"key":"e_1_2_1_29_1","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-Based API Testing for SMT Solvers. In SMT. 10 pages."},{"key":"e_1_2_1_30_1","first-page":"1","article-title":"Generative Type-Aware Mutation for Testing SMT Solvers","volume":"5","author":"Park Jiwon","year":"2021","unstructured":"Jiwon Park, Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2021. Generative Type-Aware Mutation for Testing SMT Solvers. PACMPL 5 (2021), 1-19. Issue OOPSLA.","journal-title":"PACMPL"},{"key":"e_1_2_1_31_1","first-page":"83","article-title":"HornFuzz: Fuzzing CHC solvers","author":"Sukhanova Anzhela","year":"2023","unstructured":"Anzhela Sukhanova and Valentyn Sobol. 2023. HornFuzz: Fuzzing CHC solvers. In EASE. ACM, 83-92.","journal-title":"EASE. ACM"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_2_1_33_1","first-page":"176","article-title":"Theta: A Framework for Abstraction Refinement-Based Model Checking","author":"T\u00f3th Tam\u00e1s","year":"2017","unstructured":"Tam\u00e1s T\u00f3th, \u00c1kos Hajdu, Andr\u00e1s V\u00f6r\u00f6s, Zolt\u00e1n Micskei, and Istv\u00e1n Majzik. 2017. Theta: A Framework for Abstraction Refinement-Based Model Checking. In FMCAD. IEEE Computer Society, 176-179.","journal-title":"FMCAD. IEEE Computer Society"},{"key":"e_1_2_1_34_1","first-page":"2378","article-title":"Validating SMT Solvers for Correctness and Performance via Grammar- Based Enumeration","volume":"8","author":"Winterer Dominik","year":"2024","unstructured":"Dominik Winterer and Zhendong Su. 2024. Validating SMT Solvers for Correctness and Performance via Grammar- Based Enumeration. PACMPL 8 (2024), 2378-2401. Issue OOPSLA2.","journal-title":"PACMPL"},{"key":"e_1_2_1_35_1","volume-title":"On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers. PACMPL 4","author":"Winterer Dominik","year":"2020","unstructured":"Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2020. On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers. PACMPL 4 (2020), 193:1-193:25. Issue OOPSLA."},{"key":"e_1_2_1_36_1","first-page":"718","article-title":"Validating SMT Solvers via Semantic Fusion","author":"Winterer Dominik","year":"2020","unstructured":"Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2020. Validating SMT Solvers via Semantic Fusion. In PLDI. ACM, 718-730.","journal-title":"PLDI. ACM"},{"key":"e_1_2_1_37_1","first-page":"322","article-title":"Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration","author":"Yao Peisen","year":"2021","unstructured":"Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, and Charles Zhang. 2021. Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration. In ISSTA. ACM, 322-335.","journal-title":"ISSTA. ACM"},{"key":"e_1_2_1_38_1","first-page":"1141","article-title":"Skeletal Approximation Enumeration for SMT Solver Testing","author":"Yao Peisen","year":"2021","unstructured":"Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, and Charles Zhang. 2021. Skeletal Approximation Enumeration for SMT Solver Testing. In ESEC\/FSE. ACM, 1141-1153.","journal-title":"ESEC\/FSE. ACM"},{"key":"e_1_2_1_39_1","first-page":"763","article-title":"Finding and Understanding Bugs in Software Model Checkers","author":"Zhang Chengyu","year":"2019","unstructured":"Chengyu Zhang, Ting Su, Yichen Yan, Fuyuan Zhang, Geguang Pu, and Zhendong Su. 2019. Finding and Understanding Bugs in Software Model Checkers. In ESEC\/FSE. ACM, 763-773.","journal-title":"ESEC\/FSE. ACM"},{"key":"e_1_2_1_40_1","first-page":"110","article-title":"Finding Cross-Rule Optimization Bugs in Datalog Engines","volume":"8","author":"Zhang Chi","year":"2024","unstructured":"Chi Zhang, Linzhang Wang, and Manuel Rigger. 2024. Finding Cross-Rule Optimization Bugs in Datalog Engines. PACMPL 8 (2024), 110-136. Issue OOPSLA1.","journal-title":"PACMPL"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3797104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T18:47:45Z","timestamp":1782845265000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3797104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,30]]},"references-count":40,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3797104"],"URL":"https:\/\/doi.org\/10.1145\/3797104","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,30]]}}}