Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory
Satisfiability Modulo Theory (SMT) generalizes the propositional satisfiability problem (SAT) by extending support for various first-order background theories. In this paper, we focus on the SMT problems in Non-Linear Integer Arithmetic (NIA) theory, referred to as SMT(NIA), which has wide applications in software engineering. The dominant paradigm for SMT(NIA) is the CDCL(T) framework, while recently stochastic local search (SLS) has also shown its effectiveness. However, the cooperation between the two methods has not been studied yet. Motivated by the great success of the deep cooperation of CDCL and SLS for SAT, we propose a two-layer hybrid approach for SMT(NIA). The outer-layer interleaves between the inner-layer and an independent SLS solver. In the inner-layer, we take CDCL(T) as the main body, and design a CDCL(T)-guided SLS solver, which is invoked at branches corresponding to skeleton solutions and returns useful information to improve the branching heuristics of CDCL(T). We implement our ideas on top of the CDCL(T) tactic of z3 with an SLS solver called LocalSMT, resulting in a hybrid solver dubbed HybridSMT. Extensive experiments are carried out on the standard SMT(NIA) benchmarks from SMT-LIB, where most of the instances are from real-world software engineering applications of termination and non-termination analysis. Experiment results show that HybridSMT significantly improves the CDCL(T) solver in z3. Moreover, our solver can solve 10.36% more instances than the currently best SMT(NIA) solver, and is more efficient for software verification instances.
Thu 18 AprDisplayed time zone: Lisbon change
11:00 - 12:30 | Testing 3Research Track / Journal-first Papers / Software Engineering in Practice at Grande Auditório Chair(s): José Miguel Rojas The University of Sheffield | ||
11:00 15mTalk | Do Automatic Test Generation Tools Generate Flaky Tests? Research Track Martin Gruber BMW Group, University of Passau, Muhammad Firhard Roslan University of Sheffield, Owain Parry The University of Sheffield, Fabian Scharnböck University of Passau, Phil McMinn University of Sheffield, Gordon Fraser University of Passau Pre-print | ||
11:15 15mTalk | Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory Research Track Xindi Zhang Institute of Software Chinese Academy of Science, Bohan Li Institute of Software Chinese Academy of Science, Shaowei Cai Institute of Software at Chinese Academy of Sciences | ||
11:30 15mTalk | Uncover the Premeditated Attacks: Detecting Exploitable Reentrancy Vulnerabilities by Identifying Attacker Contracts Research Track Shuo Yang Sun Yat-sen University, Jiachi Chen Sun Yat-sen University, Mingyuan Huang Sun Yat-Sen University, Zibin Zheng Sun Yat-sen University, Yuan Huang School of Data and Computer Science, Sun Yat-sen University, Guangzhou, China | ||
11:45 15mTalk | Practical Non-Intrusive GUI Exploration Testing with Visual-based Robotic Arms Research Track Shengcheng Yu Nanjing University, Chunrong Fang Nanjing University, Mingzhe Du Nanjing University, Yuchen Ling Nanjing University, Zhenyu Chen Nanjing University, Zhendong Su ETH Zurich | ||
12:00 15mTalk | Dynamic Inference of Likely Symbolic Tensor Shapes in Python Machine Learning Programs Software Engineering in Practice Pre-print | ||
12:15 7mTalk | Mutation Analysis for Evaluating Code Translation Journal-first Papers Giovani Guizzo Brick Abode, Jie M. Zhang King's College London, Federica Sarro University College London, Mark Harman Meta Platforms, Inc. and UCL, Christoph Treude Singapore Management University | ||
12:22 7mTalk | Generalized Coverage Criteria for Combinatorial Sequence Testing Journal-first Papers Achiya Elyasaf Ben-Gurion University of the Negev, Eitan Farchi IBM Haifa Research Lab, Oded Margalit Ben-Gurion University of the Negev, Gera Weiss Ben-Gurion University of the Negev, Yeshayahu Weiss Ben-Gurion University of the Negev Link to publication DOI |