Boosting Constrained Horn Solving by Unsat Core Learning
The Relational Hyper-Graph Neural Network (R-HyGNN) was introduced in [1] to learn domain-specific knowledge from program verification problems encoded in Constrained Horn Clauses (CHCs). It exhibits high accuracy in predicting the occurrence of CHCs in counterexamples. In this research, we present an R-HyGNN-based framework called MUSHyperNet. The goal is to predict the Minimal Unsatisfiable Subsets (MUSes) (i.e., unsat core) of a set of CHCs to guide an abstract symbolic model checking algorithm. In MUSHyperNet, we can predict the MUSes once and use them in different instances of the abstract symbolic model checking algorithm. We demonstrate the efficacy of MUSHyperNet using two instances of the abstract symbolic modelchecking algorithm: Counter-Example Guided Abstraction Refinement (CEGAR) and symbolic model-checking-based (SymEx) algorithms. Experimental results from a uniform selection of benchmarks across all categories from CHC-COMP show that the number of solved problems increased by 6.1%, and the average solving time decreased by 13.3%.
Mon 15 JanDisplayed time zone: London change
11:00 - 12:30 | Session 2: SAT, SMT and Automated ReasoningVMCAI at Marconi Room Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
11:00 20mTalk | Function synthesis for maximizing model counting VMCAI Thomas Vigouroux VERIMAG - UGA, Marius Bozga CNRS; Université Grenoble Alpes, Cristian Ene Verimag, Grenoble, Laurent Mounier Université Grenoble Alpes Pre-print | ||
11:20 20mTalk | Boosting Constrained Horn Solving by Unsat Core Learning VMCAI Parosh Aziz Abdulla Uppsala University, Sweden, Chencheng Liang Uppsala University, Philipp Rümmer University of Regensburg and Uppsala University | ||
11:40 20mTalk | On the Verification of a Subgraph Construction Algorithm VMCAI Lucas Böltz Univerity of Koblenz, Viorica Sofronie-Stokkermans University of Koblenz, Hannes Frey University of Koblenz | ||
12:00 20mTalk | Efficient Local Search for Nonlinear Real Arithmetic VMCAI Zhonghan Wang State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Bohua Zhan Institute of Software, Chinese Academy of Sciences, Bohan Li State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing, China, Shaowei Cai Institute of Software at Chinese Academy of Sciences | ||