Abstract
The property-directed reachability (PDR) algorithm has been one of the most successful hardware model checking algorithms powering modern formal property verification tools. Inductive generalization is the key to the efficiency of the PDR algorithm. In this paper, we present NeuroPDR, a message-passing graph neural network that learns to generalize inductive clauses to accelerate the PDR algorithm. Experiments show that on average, the integration of NeuroPDR reduces around 26.4% of the time of convergence, and the network trained on one set of benchmarks can also benefit solving another. The speed-up and transferability indicate a promising future for hybrid model checkers with machine learning methods integrated.
Guangyu (Gary) Hu
Researcher at Huawei Hong Kong Research Center, Fermat Lab
My research interests include LLM + formal verification reasoning and hardware formal verification.