Formal Verification of Parameterized Systems based on Induction
Jiaqi Xiu, Yongjian Li
TL;DR
The paper addresses the challenge of verifying parameterized systems, where verification is complicated by parameter dependence and mixed $\forall/\exists$ quantifiers. It introduces wiseParaverifier, a two-stage inductive framework consisting of invFinder for counterexample guided invariant discovery and Verifier for parameterization and proof, augmented with symmetry reduction and a type-saturation based quantifier generalization. Key contributions include the counterexample guided construction of auxiliary invariants, the Generalize heuristic for concise invariants, a merging and symmetry framework for parameterized invariants, and extensive experiments across 7 cache coherence and 10 distributed protocols demonstrating robust automated verification and readable results. The results highlight the approach’s scalability, applicability to complex protocol families, and potential to improve understanding of protocol behaviors through concise inductive proofs.
Abstract
Parameterized systems play a crucial role in the computer field, and their security is of great significance. Formal verification of parameterized protocols is especially challenging due to its "parameterized" feature, which brings complexity and undecidability. Existing automated parameterized verification methods have limitations, such as facing difficulties in automatically deriving parameterized invariants constrained by mixed Forall and Exists quantifiers, or having challenges in completing the parameterized verification of large and complex protocols. This paper proposes a formal verification framework for parameterized systems based on induction, named wiseParaverifier. It starts from small concretizations of protocols, analyzes inductive counterexamples, and constructs counterexample formulas to guide the entire process of parameterized verification. It also presents a heuristic Generalize method to quickly find auxiliary invariants, a method for promoting complex mixed quantifiers and merging parameterized invariants, and uses symmetric reduction ideas to accelerate the verification process. Experimental results show that wiseParaverifier can successfully complete automatic inductive verification on 7 cache coherence protocols and 10 distributed protocols. It has strong verification capabilities and migration capabilities, and can provide concise and readable verification results, which is helpful for learners to understand protocol behaviors.