MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved together has inspired a number of proposals, ranging from structural clustering based on the property cone of influence (COI) to leverage runtime design and verification statistics. In this paper, we present an attempt towards functional clustering of properties utilizing graph neural network (GNN) embeddings for creating effective property clusters. We propose a hybrid approach that can exploit neural functional representations of hardware circuits and runtime design statistics to speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification (MPV). Our method intelligently groups properties based on their functional embedding and design statistics, resulting in speedup in verification results. Experimental results on the HWMCC benchmarks show the efficacy of our proposal with respect to the state-of-the-art.
Code (0)
등록된 구현이 없습니다.
Tasks
Graph Neural NetworkSimilar Papers 제목 키워드 기반
Lifted Model Checking for Relational MDPs
Probabilistic model checking has been developed for verifying systems that have stochastic and nondeterministic behavior. Given a probabilistic system, a probabilistic model checker takes a property and checks whether or…
modelModel-based Reinforcement Learningreinforcement-learningReinforcement Learning (RL)NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
Formal verification is a crucial technique for ensuring the functional correctness of hardware designs. In the context of property checking, a key challenge is how to efficiently prove a user-specified property in the fa…
Property-Directed Verification of Recurrent Neural Networks
This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning.…
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
We investigate the decidability of the ${0,\infty}$ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable f…
Quantitative Verification of Neural Networks And its Security Applications
Neural networks are increasingly employed in safety-critical domains. This has prompted interest in verifying or certifying logically encoded properties of neural networks. Prior work has largely focused on checking exis…
Fairness