Advertisement
Published in:
2000 | OriginalPaper | Chapter
Induction in Compositional Model Checking
Authors : Kenneth L. McMillan, Shaz Qadeer, James B. Saxe
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper describes a technique of inductive proof based on model checking. It differs from previous techniques that combine induction and model checking in that the proof is fully mechanically checked and temporal variables (process identifiers, for example) may be natural numbers. To prove ∀n.ϕ(n) inductively, the predicate $\varphi(n-1) \Rightarrow \varphi(n)$ must be proved for all values of the parameter n. Its proof for a fixed n uses a conservative abstraction that partitions the natural numbers into a finite number of intervals. This renders the model finite. Further, the abstractions for different values of n fall into a finite number of isomorphism classes. Thus, an inductive proof of ∀n.ϕ(n) can be obtained by checking a finite number of formulas on finite models. The method is integrated with a compositional proof system based on the SMV model checker. It is illustrated by examples, including the N-process “bakery” mutual exclusion algorithm.