An Automatic Proving Approach to Parameterized Verification
2018
Formal verification of parameterized protocols such as cache coherence protocols is a significant challenge. In this article, we propose an automatic proving approach and its prototype paraVerifier to handle this challenge within a unified framework as follows: (1) To prove the correctness of a parameterized protocol, our approach automatically discovers auxiliary invariants and the corresponding dependency relations among the discovered invariants and protocol rules from a small instance of the to-be-verified protocol, and (2) the discovered invariants and dependency graph are then automatically generalized into a parameterized form and sent to the theorem prover, Isabelle. As a side product, the final verification result of a protocol is provided by a formal and human-readable proof. Our approach has been successfully applied to a number of benchmarks, including snoopying-based and directory-based cache coherence protocols.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
32
References
6
Citations
NaN
KQI