Presenting at VMCAI 2024 in London
In January 2024, I attended the 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024) in London, United Kingdom. At the conference, I presented our accepted paper, “Boosting Constrained Horn Solving by Unsat Core Learning.”
VMCAI at POPL 2024
VMCAI 2024 took place on January 15–16, 2024, as an in-person conference at the Institution of Engineering and Technology (IET), Savoy Place in London. It was one of the co-hosted conferences within POPL 2024, whose wider programme ran from January 14–20 and brought together research across programming languages, verification, logic, and related areas.
VMCAI provides a forum for work spanning program verification, model checking, and abstract interpretation, with an emphasis on interaction between these communities and on hybrid methods that combine their ideas. The 2024 programme covered topics including SAT and SMT solving, automated reasoning, security and privacy, infinite-state systems, runtime verification, probabilistic and quantum programs, neural networks, and program analysis.
Presenting Our Paper
Together with Parosh Aziz Abdulla and Philipp Rümmer, I presented our paper “Boosting Constrained Horn Solving by Unsat Core Learning.” The work used the Relational Hyper-Graph Neural Network (R-HyGNN) to predict minimal unsatisfiable subsets—unsat cores—of verification problems encoded as Constrained Horn Clauses (CHCs).
These predictions are used to guide symbolic model-checking algorithms toward the clauses most relevant to solving a problem. We evaluated the approach with both counterexample-guided abstraction refinement and symbolic-execution-based algorithms, showing that learned unsat-core information could help solve more benchmarks while reducing average solving time.
I gave the conference presentation during the SAT, SMT and Automated Reasoning session on January 15. The paper, BibTeX entry, DOI record, and presentation slides are available online.
Moments from London
