Exploring properties and limitations of Graph Neural Networks (GNNs) in Software Verification

Abstract: This study analyzes how applicable Graph Neural Networks (GNNs) can be used for learning the labels of Horn graphs that are generated from Constrained Horn Clauses (CHCs) using Eldarica. To answer this question, 121 mono-direction edge layer graphs and hyper-edge graphs are prepared to be trained and validated and tested, weights per 10 epochs and losses are collected and visualized in 6 scenarios. From the experiments, we can observe that GNNs can learn particular features to classify the labels of nodes but the learning process still gets stuck and causes the divergence of the losses. Also, increasing the number of the message passing layers and number of the graphs can cause significant challenges for the learning process. With the strong representational learning capacity, Graph Neural Networks (GNNs) can be explored for even more uses in the future.