There is a recent trend toward the automation of the model checking and computer program verification process. The program or the model being verified and its verifiable property need to be restricted in the finite state spaces. The authors address the set-based reduction method for automatic computer program verification. The authors develop two methods of implementing state matching: one using quantifiers and another that is quantifier-free. The authors use two case studies to investigate the relationship between image-based and equivalence-based state matching, namely DVE (native language of DIVINE) models and random models. Further, the authors employ the DVE language for open systems, set-based reduction with explicit sets, set-based reduction with symbolic sets, equivalence-based versus image-based state matching and image versus equivalence using linear search, and experiments with witness-based matching resolution in both DVE and random models.
展开▼
