Invited Talk at ISTA
On May 11, 2024, I visited the Institute of Science and Technology Austria (ISTA) in Klosterneuburg to give an invited talk to the Thomas Henzinger Group. I was honored to receive the invitation from Emily Yu, who was then a postdoctoral researcher in the group. Emily’s research in formal methods, automated reasoning, hardware model checking, and certification closely connected with my own work on machine learning for program verification. The Henzinger group develops mathematical foundations for the design and verification of complex hardware and software systems, with research spanning model checking, autonomous and cyber-physical systems, and trustworthy AI. These shared interests made ISTA a particularly fitting place to exchange ideas, and I am very grateful to Emily for inviting and hosting me.
Guiding CHC Solving with Graph Neural Networks
My talk, “Guiding Constraint Horn Clauses Solving using Graph Neural Networks,” focused on how deep learning can support formal verification. I first introduced how program-verification problems can be encoded as Constrained Horn Clauses (CHCs) and why the order in which clauses are processed can influence the performance of CHC solvers.
I then presented our learning-based approach to this ranking problem. We use minimal unsatisfiable subsets of CHCs as supervision and represent the clauses with the Relational Hyper-Graph Neural Network (R-HyGNN). The resulting predictions estimate which clauses are most likely to belong to an unsatisfiable core and can guide solving procedures such as counterexample-guided abstraction refinement and symbolic execution. The visit offered a valuable opportunity to discuss how graph learning, automated reasoning, and formal verification can complement one another with researchers working on closely related questions.
The presentation slides are available online. Related technical details can also be found in our paper, “Boosting Constrained Horn Solving by Unsat Core Learning”.
Moments from ISTA
