POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 11:20 - 11:40 at Marconi Room - Session 2: SAT, SMT and Automated Reasoning Chair(s): David Monniaux

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 Jan

Displayed 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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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