Presenting at HCVS 2024 in Luxembourg
In April 2024, I attended the 11th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2024) in Luxembourg City, Luxembourg. At the workshop, I gave a presentation on our previously published work, “Boosting Constrained Horn Solving by Unsat Core Learning.”
HCVS at ETAPS 2024
HCVS 2024 was held on April 7, 2024, in the Vianden room at Parc Hotel Alvisse in Luxembourg City. It was a satellite workshop of ETAPS 2024, organized by the University of Luxembourg and its Interdisciplinary Centre for Security, Reliability and Trust (SnT).
HCVS brings together researchers from constraint and logic programming, program verification, and automated deduction to exchange work on Horn-clause-based analysis, verification, and synthesis. The 2024 workshop also hosted CHC-COMP, the competition for constrained Horn clause solvers.
Presenting at HCVS
At HCVS, I presented “Boosting Constrained Horn Solving by Unsat Core Learning,” joint work with Parosh Aziz Abdulla and Philipp Rümmer. The paper had previously been published at VMCAI 2024 and was included in the HCVS programme as a presentation-only contribution.
The work uses the Relational Hyper-Graph Neural Network (R-HyGNN) to predict minimal unsatisfiable subsets—unsat cores—of program-verification problems encoded as Constrained Horn Clauses (CHCs). These predictions guide symbolic model-checking algorithms toward the clauses most relevant to the solving process. Presenting the work at HCVS provided an opportunity to discuss it with a community focused specifically on Horn-clause-based verification and synthesis.
The paper, BibTeX entry, DOI record, and HCVS presentation slides are available online.
Moments from Luxembourg
