| Title | Accelerated Verification of Parametric Protocols with Decision Trees |
| Publication Type | Conference Paper |
| Year of Publication | 2020 |
| Authors | Li, Yongjian, Cao, Taifeng, Jansen, David N., Pang, Jun, Wei, Xiaotao |
| Conference Name | 2020 IEEE 38th International Conference on Computer Design (ICCD) |
| Date Published | oct |
| Keywords | Acceleration, cache coherence protocols, Coherence, composability, compositionality, Conferences, Decision trees, Design methodology, formal methods, knowledge based systems, machine learning, parameterized verification, policy-based governance, privacy, protocol verification, Protocols, pubcrawl |
| Abstract | Within a framework for verifying parametric network protocols through induction, one needs to find invariants based on a protocol instance of a small number of nodes. In this paper, we propose a new approach to accelerate parameterized verification by adopting decision trees to represent the state space of a protocol instance. Such trees can be considered as a knowledge base that summarizes all behaviors of the protocol instance. With this knowledge base, we are able to efficiently construct an oracle to effectively assess candidates of invariants of the protocol, which are suggested by an invariant finder. With the discovered invariants, a formal proof for the correctness of the protocol can be derived in the framework after proper generalization. The effectiveness of our method is demonstrated by experiments with typical benchmarks. |
| DOI | 10.1109/ICCD50377.2020.00073 |
| Citation Key | li_accelerated_2020 |
Accelerated Verification of Parametric Protocols with Decision Trees