A Constrained Horn Clause (CHC) is a specific type of logic formula that contains uninterpreted predicates. CHC formulas are often used by static program analyzers to encode program properties, which are then verified using CHC solvers. The solvers themselves are complex tools and may contain bugs, which can lead to verifying unsafe programs, flagging safe programs as unsafe, or providing analyzers with incorrect invariants and counterexamples. It is, therefore, crucial to develop techniques for systematically testing CHC solvers.
In this paper, we present the first interrogation-testing technique for CHC solvers, which we implement in a tool called HornGator. Our technique uses witnesses generated by the solver under test to form new CHC instances. It also integrates a knowledge base maintaining a history of past solver queries. All this information helps HornGator generate more diverse instances, thereby improving its bug-finding effectiveness. As a result, HornGator found 21 unique bugs in five state-of-the-art CHC solvers, all of which are confirmed by the developers, 18 are fixed, and eight are of the highest severity.
Thu 9 JulDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:30 | Testing 3Research Papers / Industry Papers / Tool Demonstrations / Ideas, Visions and Reflections at MB 1.210 Chair(s): Nimmi Weeraddana University of Calgary, Canada | ||
10:30 20mTalk | ACME: Automated Clause Mapping Engine for Testing Emerging Database Systems Research Papers Yuancheng Jiang National University of Singapore, Jianing Wang Shandong University, Chuqi Zhang National University of Singapore, Roland H. C. Yap National University of Singapore, Zhenkai Liang National University of Singapore, Manuel Rigger National University of Singapore DOI Pre-print | ||
10:50 20mTalk | Interrogation Testing of CHC Solvers Research Papers David Kaindlstorfer TU Wien, Austria, Anastasia Isychev TU Wien, Valentin Wüstholz ConsenSys, Maria Christakis TU Wien Pre-print | ||
11:10 20mTalk | RAT: Retrieval-Augmented Testing of Certificate Revocation List Parsers in TLS Implementations Research Papers Chu Chen Qufu Normal University, Qianxin Cheng Qufu Normal University, Pinghong Ren Qufu Normal University, Hairong Yu Qufu Normal University, Cong Tian Xidian University, Zhenhua Duan Xidian University, Xu Lu Xidian University, Bin Yu Xidian University, WenSheng Wang Xidian University, Jin Liu Xi'an University of Technology Pre-print | ||
11:30 10mTalk | Software Testing Beyond Closed Worlds: Open-World Games as an Extreme Case Ideas, Visions and Reflections Yusaku Kato Ritsumeikan University, Norihiro Yoshida Ritsumeikan University, Erina Makihara Ritsumeikan University, Katsuro Inoue Ritsumeikan University Pre-print | ||
11:40 20mTalk | AstraGame: Effective and Efficient VLM Agent Serving for Large-Scale Game Testing in an Industry Setting Industry Papers Yuzhe Guo Peking University, Haochuan Lu Tencent, Mengzhou Wu Peking University, Ting Xiong Tencent Inc., Yuetang Deng Tencent, Dezhi Ran Peking University, Wei Yang UT Dallas, Tao Xie Peking University | ||
12:00 10mTalk | ScalerEval: Automated and Consistent Evaluation Testbed for Auto-scalers in Microservices Tool Demonstrations Shuaiyu Xie School of Computer Science, Wuhan University, China, Yang Luo Wuhan University, Yuzhen Tan Wuhan University, Yunqing Yong Wuhan University, Xiaosong Huang Peking University, Jian Wang Wuhan University, Bing Li Wuhan University | ||
12:10 20mTalk | WalleTruth: Visual-oriented Software Testing for Web3 Wallet Browser Extensions Research Papers Xiaohui Hu Huazhong University of Science and Technology, Ningyu He Hong Kong Polytechnic University, Haoyu Wang Huazhong University of Science and Technology DOI Authorizer link | ||